proposition: Lemma apply_noCycle_left {A} {noconf : NoCyclePackage A} (p q : A) {B : p = q -> Type} : NoCycle p q -> (forall H : p = q, B H).
proof: Proof. intros. destruct (noCycle H H0). Defined.
imports: Equations.Init Equations.CoreTactics Coq(Extraction Relation_Definitions) Equations.Prop.Logic