proposition: Lemma restr_range1 f x: fgraph f -> sub x (domain f) -> sub (range (restr f x)) (range f).
proof: Proof. move=> pa pb t/funI_P [u /funI_P [z zx -> ->]]; aw. exact: (inc_V_range pa (pb _ zx)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)