proposition: Lemma exercise4_4b g x: singletonp x -> graph_morph (direct_image^~x) intersectionb g.
proof: Proof. move=> [y ->]; set_extens t. move => /dirim_P [a /set1_P ->]. case: (emptyset_dichot g) => gne; first by rewrite gne setIb_0 => /in_set0. move => pi; apply: setIb_i. move /domain_set0P: gne => [u udg]. pose ff i := direct_image (Vg g i) (singleton y). exists (J u (ff u)); apply /funI_P; ex_tac. aw; move => i idg; rewrite LgV//; apply/dirim_P; exists y; fprops. exact (setIb_hi pi idg). set f := Lg _ _. have dfdf: domain f = domain g by rewrite /f; aw. case: (emptyset_dichot g) => gne. by rewrite /f gne domain_set0 /Lg funI_set0 setIb_0 => /in_set0. move => ti; apply /dirim_P; exists y; first by fprops. apply/(setIb_P gne) => i idg; move: (idg); rewrite -dfdf=> idf. by move: (setIb_hi ti idf); rewrite LgV//; move /dirim_P => [u /set1_P ->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)