proposition: Lemma fun_image_exten x f g: (forall t, inc t x -> f t = g t) -> fun_image x f = fun_image x g.
proof: Proof. by move => h; set_extens t; move => /funI_P [z zx ->]; apply /funI_P; ex_tac; rewrite h. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)