proposition: Lemma Fix2_F_eq' : forall xx' (r : Acc R xx'), F (fun y y' (p : R (y, y') (fst xx', snd xx')) => Fix2_F (x:=y) (x':=y') (Acc_inv r (match xx' return R _ (fst xx', snd xx') -> R _ xx' with | (x, x') => fun p => p end p))) = Fix2_F (x:=fst xx') (x':=snd xx') (match xx' return Acc R xx' -> Acc R (fst xx', snd xx') with | (x, x') => fun p => p end r).
proof: Proof. destruct r using Acc_inv_dep. match goal with | [ x : (A * B)%type |- _ ] => destruct x; auto end. 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