proposition: Lemma Fix2_0_eq : forall (x:A) (x':B), Fix2 x x' = F (fun (y:A) (y':B) (p:R (y, y') (x, x')) => Fix2 y y').
proof: Proof. intros x x'; unfold Fix2. rewrite <- Fix2_F_eq. apply F_ext; intros. apply Fix2_F_inv. 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