proposition: Lemma Fix2_F_inv : forall (x:A) (x':B) (r s:Acc R (x, x')), Fix2_F r = Fix2_F s.
proof: Proof. intros x x'. exact (@Fix2_F_inv' (x, x')). Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Coq.Setoids.Setoid Coq.Program.Program Coq.Program.Wf Coq.Arith.Wf_nat Coq.Classes.Morphisms Coq.Init.Wf Fiat.Common.Telescope.Core Fiat.Common.Telescope.Instances Fiat.Common.Telescope.Equality Fiat.Common Fiat.Common.Equality Fiat.Common.Wf1