proposition: Lemma extendsC_pr (a b a' b':Set) (g:a'->b')(f:a->b)(H: sub a a'): extendsC g f H -> forall x:a, Ro (f x) = Ro(g (inclusionC H x)).
proof: Proof. move=> [e1]; rewrite /agreeC => eq x; rewrite eq. by rewrite /restrictionC composeC_ev inclusionC_identity. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)