proposition: Lemma funI_exten f1 f2 X: {inc X, f1 =1 f2} -> fun_image X f1 = fun_image X f2.
proof: Proof. by move => hyp; set_extens t ; move => /funI_P [y ya ->]; apply/funI_P; ex_tac; symmetry;apply: hyp. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)