proposition: Lemma Eq_restriction1 f x: sub x (source f) -> injection f -> x \Eq (Vfs f x).
proof: Proof. move=> wsf bf; have h:=(restriction1_fb bf wsf). by exists (restriction1 f x); split => //; rewrite/restriction1; aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)