proposition: Lemma FixV_2V_eq A A' (B : A * A' -> Telescope) (R : A * A' -> A * A' -> Prop) (Rwf : well_founded R) (P : forall aa', flattenT (B aa') Type) (F : forall xx', (forall yy', R yy' xx' -> flatten_forall (P yy')) -> flatten_forall (P xx')) (F' : forall x x', (forall y y', R (y, y') (x, x') -> flatten_forall (P (y, y'))) -> flatten_forall (P (x, x')) := fun x x' (f : forall y y', R (y, y') (x, x') -> flatten_forall (P (y, y'))) => F (x, x') (fun yy' => match yy' return R yy' _ -> flatten_forall (P yy') with | (y, y') => f y y' end)) (F_ext : forall xx' (f g : forall yy', R yy' xx' -> flatten_forall (P yy')), (forall yy' (p : R yy' xx'), flatten_forall_eq (f yy' p) (g yy' p)) -> flatten_forall_eq (@F xx' f) (@F xx' g)) : forall aa', flatten_forall_eq (@Fix (A * A') R Rwf (fun aa' => flatten_forall (P aa')) F aa') (match aa' with | (a, a') => @Fix2 A A' R Rwf (fun aa' => flatten_forall (P aa')) F' a a' end).
proof: Proof. intro aa'; induction (Rwf aa'). destruct_prods. etransitivity; [ solve [ apply FixV_eq; intros; destruct_prods; apply F_ext; intros; destruct_prods; auto ] | ]. etransitivity; [ | solve [ symmetry; apply (@Fix2V_eq A A' B R Rwf P F'); intros; destruct_prods; apply F_ext; intros; destruct_prods; eauto ] ]. apply F_ext; intros; destruct_prods; eauto. 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