Function derive_ctor_inj 

pub fn derive_ctor_inj(
    ctx: &Context,
    ind: &str,
    ctor: &str,
) -> KernelResult<(Term, Term)>

C_inj : Π(A…). Π(x⃗). Π(y⃗). Eq (I A…) (C A… x⃗) (C A… y⃗) → (x₀ = y₀ ∧ … ∧ x_{m-1} = y_{m-1})

Lean’s C.inj — the constant injection h produces. It is derive_no_confusion at P := the conjunction, applied to the function that just repackages the equations, so it needs no defaulted projection and therefore no inhabitant of the other constructors’ fields (the reason a hand-written pred-style projection cannot do this in general).

NOT derived here: Lean’s C.injEq, which states the same fact as an EQUALITY of propositions ((C x⃗ = C y⃗) = (x⃗ = y⃗)) and so needs propext. The implication above is the propext-free content.