proposition: Lemma agrees_same_restrictionC (a a' b x:Set) (f:a->b)(g:a'->b) (Ha: sub x a)(Hb: sub x a'): agreeC f g Ha Hb -> restrictionC f Ha =1 restrictionC g Hb.
proof: Proof. move => ag z; apply: R_inj; apply: ag. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)