Function derive_no_confusion 

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

I_noConfusion : Π(A…). Π(P : Type 0). Π(a b : I A…). Eq (I A…) a b → I_noConfusionType A… P a b

The proof half. It is ONE transport: noConfusionType P a a is inhabited on the DIAGONAL (for each constructor, λk. k (refl x₀) … (refl x_{m-1})), and J carries that along the equation to noConfusionType P a b. Instantiating P gives both halves of what Lean’s injection and cases h use — P := False is constructor disjointness, P := (xₖ = yₖ) is field-k injectivity (see derive_ctor_inj).

A definition, kernel-checked: nothing here is assumed.