proposition: Lemma Acc_prop i (x y : Acc i) : x = y.
proof: Proof. revert y. induction x as [y Accy IHy]. intros [Accy']. apply ap. apply funext. intros H. apply funext. intros H'. apply IHy. Qed.
imports: Coq(Extraction CRelationClasses) Equations.Init Equations.CoreTactics Equations.Type.Logic Equations.Type.FunctionalExtensionality Equations.Type.Relation Equations.Type.Relation_Properties