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 (inverse eq)). Defined.
imports: Equations.Init Equations.CoreTactics HoTT.Basics.Trunc HoTT.HSet Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties Equations.HoTT.WellFounded