proposition: Lemma nsv_rec: S =2o fun a b => osups (doubleI_rg S a b).
proof: Proof. move => a b oa ob. rewrite {1}/S (doubleI_tdef_rec2 _ oa ob); congr osups. rewrite /doubleI_restr2; set f := Lfs _ _. have ha: surjection f by apply:Lfs_surjective. have hb: source f = (doubleI_F a b) by rewrite Lfs_source. rewrite - (surjective_pr0 ha). set_extens t. move/(Imf_P (proj1 ha)) => [u uF ->]; rewrite hb in uF. rewrite (Lfs_V _ uF); apply/setU2_P; case/setU2_P: uF. by move/setX_P =>[pp /set1_P -> ub]; right;apply:funI_i. by move/setX_P =>[pp ua /set1_P ->]; left;apply:funI_i. case/setU2_P=>/funI_P [z zab ->];apply /(Imf_P (proj1 ha)). have h: inc (J z b) (doubleI_F a b). by apply/setU2_P; right; apply:setXp_i; fprops. by exists (J z b); [ ue | rewrite (Lfs_V _ h); aw]. have h: inc (J a z) (doubleI_F a b). by apply/setU2_P; left; apply:setXp_i; fprops. by exists (J a z); [ ue | rewrite (Lfs_V _ h); aw]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)