proposition: Lemma exercise4_1a g: sgraph g -> (functional_graph g <-> {morph inverse_image g : x y / x \cap y}).
proof: Proof. move=> gg. have gig: sgraph (inverse_graph g) by fprops. split. move=> fgg x y; set_extens t. move /iim_graph_P => [u /setI2_P [ux uy] jg]. apply /setI2_P;split;apply /iim_graph_P; ex_tac. move /setI2_P => [ /iim_graph_P [u ux ua] /iim_graph_P [v vx va]]. rewrite -(fgg _ _ _ ua va) in vx. apply /iim_graph_P; exists u; fprops. move=> hyp x y y' gxy gxy'. move: (hyp (singleton y)(singleton y')). set u:= _ \cap _ => hyp1. have:inc x (inverse_image g u). rewrite /u hyp1;apply: setI2_i; apply /iim_graph_P. exists y; fprops. exists y'; fprops. by move /iim_graph_P => [t /setI2_P [/set1_P <- /set1_P <-]]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)