proposition: Lemma dirim_restr2 f a: fgraph f -> sub a (domain f) -> direct_image (restr f a) a = direct_image f a.
proof: Proof. move => fgf df; move: (restr_fgraph f a)=> fgf'. have df': sub a (domain (restr f a)) by rewrite restr_d. by rewrite - (dirim_restr fgf' df') -(dirim_restr fgf df) double_restr //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)