proposition: Lemma exercise6_6d G H: equivalence G -> equivalence H -> substrate G = substrate H -> G \cg H = H \cg G -> (G \cg H) = intersection(Zo (powerset (coarse (substrate G))) (fun W => [/\ equivalence W, sub G W & sub H W])).
proof: Proof. move=> eG eH sG cGH. set (E:= substrate G). have sGE: sub G (coarse E) by apply: sub_coarse. have sHE: sub H (coarse E) by rewrite /E sG; apply: sub_coarse. move: (exercise6_6c eG eH sG)=> [sGc sHc lew]. set_extens t => ts. apply: setI_i. exists (coarse E); apply: Zo_i; first by apply: setP_Ti. split=> //;apply: proj1 (coarse_equivalence E). by move=> y /Zo_P [_ [ey gy hy]]; apply: (lew _ ey gy hy). move: cGH;rewrite - exercise6_6a // => cGH. apply: (setI_hi (y:=(G \cg H)) ts); apply: Zo_i; last by done. apply /setP_P;rewrite /E - (exercise6_6b eG eH sG); apply: sub_coarse=>//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)