proposition: Lemma apply_noCycle_right@{i j|} {A : Type@{i}} {noconf : NoCyclePackage A} (p q : A) {B : p = q -> Type@{j}} : NoCycle q p -> (forall H : p = q, B H).
proof: Proof. intros noc eq. destruct (noCycle noc (id_sym eq)). Defined.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.Relation Equations.Type.Relation_Properties Equations.Type.WellFounded