Expand comment

Author: nomeata

src/Lean/Meta/Constructions/NoConfusion.lean

@@ -288,8 +288,13 @@ def Vec.cons.noConfusion.{u_1, u} : {α : Type u} → {P : Sort u_1} →
   → P
 ```
 
-We specialize to homogeneous equalities here because it is the common case, used by `injection` and
-`Meta.mkNoConfusion`. Heterogeneous uses still use the general `noConfusion` declaration above.
+These are specialized to equal parameters. The main use of these theorems is `injection` through
+`Meta.mkNoConfusion`, which deals with homogeneous equalities, so no need for the generality.
+
+These still accept a heterogeneous equality between the two constructor applications: if we tried
+to phrase this theroem with a homogeneous equality, this would force those constructor fields that
+appear in indices to be equal, which is too strong: we can have homogenenous equalities between
+two constructor applications with different fields but same indices.
 -/
 def mkNoConfusionCtors (declName : Name) : MetaM Unit := do
   -- Do not do anything unless can_elim_to_type.