proposition: Lemma doubleI_tdef_rec T: doubleI_fix1 T (doubleI_tdef T).
proof: Proof. move => a b oa ob. move:(OS_succ oa) (OS_succ ob) => h1 h2. pose T' := (fun p f => T (P p) (Q p) f). move:(doubleI_correct T' h1 h2)=>h; move:(h) => [/proj1 ha hb hc]. set E := (osucc a \times osucc b). have H: forall p, inc p E -> doubleI_tdef T (P p) (Q p) = Vf (doubleI_transdef (osucc a) (osucc b) T') p. move => p /setX_P[ pp /(oltP h1) /oleSltP ua /(oltP h2) /oleSltP vb]. move:(doubleI_correct T' (proj31 ua) (proj31 vb)) => h'. rewrite /doubleI_tdef (doubleI_unique3 ua vb h h') restriction1_V // ? pp //. rewrite hb; apply/setX_Slr; [ exact (proj33 ua) | exact (proj33 vb)]. rewrite -{1} pp;apply:setXp_i; fprops. have h5:inc (J a b) E by apply:setXp_i; fprops. have h6: sub (doubleI_E a b) E by apply:doubleI_E_sub; fprops. rewrite -{1} (pr2_pair a b) -{1} (pr1_pair a b) (H _ h5) (hc _ h5) /T'; aw. rewrite (Lfs_restriction1 ha); try ue;congr T. by apply:Lfs_exten => p /h6 pe; rewrite (H _ pe). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)