proposition: Lemma Eq_F_doubleE F a b A B : inc a F -> inc b F -> a <> b -> sub A F -> sub F B -> F \Eq (coarse F) -> A \Eq (B -s F) -> F \Eq B.
proof: Proof. move => aF bR anb sAF sFB eFF /EqS [g [[[fg gi] _] sg tg]]. apply:CantorBernstein; first by apply: set_le_t. have ra: B <=s B \times B. exists (Lf (J a) B (B \times B)). saw; apply: lf_injective; first by move => t tB; apply:setXp_i; fprops. by move => u v _ _ /=/pr2_def. have rb: B <=s F \times F. exists (Lf( fun z => (Yo (inc z F) (J a z) (J b (Vf g z)))) B (F\times F)). saw; apply: lf_injective. move => x xb /=; Ytac h; apply: setXp_i => //; apply: sAF; Wtac. by rewrite sg; apply/setC_P. move => u v uB vB /=; Ytac ha; Ytac hb => /pr12_def [hc hd]//. - by case: anb. - by move: hd;apply: gi; rewrite sg; apply/setC_P. have rc:=(set_le_i2 rb (EqS eFF)). have rd: coarse B <=s coarse F. move: rc =>[h [[fh hi] sh tf]]. exists (Lf (fun z => (J (Vf h (P z)) (Vf h (Q z)))) (coarse B) (coarse F)). saw; apply: lf_injective. move => z /setX_P[pz za ab]; apply:setXp_i; Wtac. move => u v /setX_P [pu ua ub]/setX_P[pv va vb] /pr12_def [esa sb]. apply:(pair_exten pu pv); apply: hi; ue. exact:(set_leT ra (set_le_i2 rd (EqS eFF))). Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)