proposition: Lemma exercise4_4c: exists z, not {morph (direct_image ^~z): x y / x \cap y}.
proof: Proof. exists C2. set (G:= doubleton(J C0 C0)(J C1 C1)); set (H:= doubleton(J C0 C1)(J C1 C0)). move => h; move: {h} (h G H). have ->: direct_image G C2 = C2. set_extens u. move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h); fprops. case /set2_P => h; apply /dirim_P; exists u; rewrite h /G; fprops. have -> :direct_image H C2 = C2. set_extens u. move=> /dirim_P [v vz /set2_P] [] h; rewrite (pr2_def h); fprops. case /set2_P => ->; apply /dirim_P; [ exists C1 | exists C0]; rewrite /H;fprops. rewrite setI2_id => bad. move: inc_C0_C2; rewrite -bad; move/dirim_P => [t _ /setI2_P[pa]]. have : P (J t C0) = Q (J t C0) by case/set2_P: pa => ->; aw. aw => ->; case/set2_P => h; [move: (pr2_def h) | move: (pr1_def h)]; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)