proposition: Lemma apply_noConfusion@{i j|} {A : Type@{i}} {noconf : NoConfusionPackage A} (p q : A) {B : p = q -> Type@{j}} : (forall e : NoConfusion p q, B (noConfusion e)) -> (forall e : p = q, B e).
proof: Proof. intros. generalize (noConfusion_retr e). destruct e. intros eq. destruct eq. apply X. Defined.
imports: Equations.Init Equations.CoreTactics HoTT.Basics.Trunc HoTT.HSet Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded