proposition: Lemma function_extends_restC (x a b:Set) (f:a->b)(H:sub x a): extendsC f (restrictionC f H) H.
proof: Proof. split; fprops. move => t; rewrite /restrictionC compositionC_A 2! composeC_ev. rewrite inclusionC_compose; congr (Ro (f _)). by apply: R_inj; rewrite B_eq B_eq. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)