proposition: Lemma exercise3_2 G X: sgraph G -> ( sub X (domain G) <-> sub X (direct_image (inverse_graph G) (direct_image G X))).
proof: Proof. move=> gG. split; move=> hyp t ts; move: (hyp _ ts). move/(domainP gG)=> [y Jg]; apply/dirim_P;exists y. apply/dirim_P; ex_tac. by apply/igraph_pP. move/dirim_P => [x _] /igraph_pP h; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)