proposition: Lemma exercise3_7 G: sgraph G -> (fgraph G <-> forall X, sub (direct_image G (inverse_image G X)) X).
proof: Proof. move=>gG; split. move=> fgG X x /dirim_P [y /iim_graph_P [u ux pug] pxg]. by rewrite (fgraph_pr fgG pxg pug). move=> hyp; split =>// x y xG yG sP. move:(gG _ xG) (gG _ yG)=> px py. apply: pair_exten=>//; apply: set1_eq. apply: (hyp (singleton (Q y))). apply/dirim_P; exists (P x); last by rewrite px. by apply /iim_graph_P; exists (Q y); fprops; rewrite sP py. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)