Function derive_no_confusion_type 

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

I_noConfusionType : Π(A…). Π(P : Type 0). I A… → I A… → Type 0

The type-level half of constructor disjointness, computed by cases on BOTH arguments:

noConfusionType P (C x⃗) (C y⃗) ⤳ (x⃗ = y⃗ → P) → P     -- the same constructor: injectivity
noConfusionType P (C x⃗) (D y⃗) ⤳ P                    -- different ones: anything follows

Lean’s is {α} → Sort v → I α → I α → Sort v; ours pins P to Type 0 because the prelude’s Eq quantifies over a Type 0 carrier, which is the same bound its companion noConfusion runs into. A Prop goal still passes by cumulativity, which is the case cases h/injection actually needs.

Match here is positional with no patterns and no wildcard, so an n-constructor inductive genuinely spells out all n² arms — that is not a shortcut, it is the shape of the term.