proposition: Lemma Fix2_F_eq : forall x x' (r : Acc R (x, x')), F (fun y y' (p : R (y, y') (x, x')) => Fix2_F (x:=y) (x':=y') (Acc_inv r p)) = Fix2_F (x:=x) (x':=x') r.
proof: Proof. intros x x'. exact (@Fix2_F_eq' (x, x')). Defined.
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