proposition: Lemma Fix2_F_inv' : forall xx' (r s:Acc R xx'), Fix2_F (match xx' return Acc R xx' -> Acc R (fst xx', snd xx') with | (x, x') => fun p => p end r) = Fix2_F (match xx' return Acc R xx' -> Acc R (fst xx', snd xx') with | (x, x') => fun p => p end s).
proof: Proof. intro xx'; induction (Rwf xx'); intros. rewrite <- (Fix2_F_eq' r); rewrite <- (Fix2_F_eq' s); intros. destruct_prods. apply F_ext; auto. 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