proposition: Lemma Acc_prop `{Funext} {A} (R : Relation A) i (x y : Acc R i) : x = y.
proof: Proof. revert y. induction x as [y Accy IHy]. intros [Accy']. apply ap. funext H'. funext H''. apply IHy. Qed.
imports: Equations.Init Equations.CoreTactics Equations.HoTT.Logic Equations.HoTT.Relation Equations.HoTT.Relation_Properties HoTT.Basics.Tactics