proposition: Lemma apply_noConfusion {A} {noconf : NoConfusionPackage A} (p q : A) {B : p = q -> Type} : (forall H : NoConfusion p q, B (noConfusion H)) -> (forall H : p = q, B H).
proof: Proof. intros. generalize (noConfusion_retr H). intros e. destruct e. apply X. Defined.
imports: Equations.Init Equations.CoreTactics Coq(Extraction Relation_Definitions) Equations.Prop.Logic