proposition: Lemma Acc_pi (A : Type) (R : relation A) i (x y : Acc R i) : x = y.
proof: Proof. revert y. induction x using Acc_dep. intros. destruct y. f_equal. extensionality y. extensionality H'. apply H. Qed.
imports: Coq(Wf_nat Relations) Coq(Wellfounded Relation_Definitions) Coq(Relation_Operators Lexicographic_Product Wf_nat) Equations(Init Signature) Equations.CoreTactics Equations.Prop.Classes Equations.Prop.EqDec Equations.Prop.DepElim Equations.Prop.Constants