proposition: Lemma inverse_direct_imageg r x: sgraph r -> sub x (domain r) -> sub x (inverse_image r (direct_image r x)).
proof: Proof. move=> gt xd t tx. move /funI_P: (xd _ tx)=> [y yr eq]. have aux:inc (J t (Q y)) r by rewrite eq (gt _ yr). apply/iim_graph_P;ex_tac;apply/dirim_P; ex_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)