proposition: Lemma restriction2C_pr (a a' b b':Set) (f:a->b)(Ha:sub a' a) (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b') (x:a'): Ro (restriction2C H x) = Vf (acreate f) (Ro x).
proof: Proof. rewrite /restriction2C B_eq; set (y:=inclusionC Ha x). have RR: (Ro y = Ro x) by rewrite /y/inclusionC B_eq. by rewrite -RR acreate_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)