proposition: Lemma restriction2C_pr1 (a a' b b':Set) (f:a->b) (Ha:sub a' a)(Hb:sub b' b) (H: forall u:a', inc (Ro (f (inclusionC Ha u))) b'): f \o (inclusionC Ha) =1 (inclusionC Hb) \o (restriction2C H).
proof: Proof. by move=> t; rewrite /restriction2C; apply: R_inj; rewrite B_eq B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)