proposition: Lemma extension_injective x f g a b: domain f = domain g -> ~ (inc x (domain f)) -> (f +s1 (J x a) = g +s1 (J x b)) -> f = g.
proof: Proof. move=> seq nixsf sv. set_extens t => tf. have: inc t (g +s1 J x b) by rewrite - sv; fprops. by case /setU1_P => // ta;case: nixsf; apply /funI_P; ex_tac; rewrite ta;aw. have: inc t (f +s1 J x a) by rewrite sv; fprops. case /setU1_P => // ta. by case: nixsf; rewrite seq;apply /funI_P; ex_tac; rewrite ta;aw. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)