proposition: Lemma function_exten f g: function f -> function g -> source f = source g -> target f = target g -> {inc (source f), f =1f g} -> f = g.
proof: Proof. move=> ff fg e1 r2 e2; apply: function_exten3=> //. set_extens x => xg. have Pf : (inc (P x) (source f)) by Wtac. by rewrite (in_graph_Vf ff xg) (e2 _ Pf); Wtac; rewrite -e1. have Pg : (inc (P x) (source f)) by rewrite e1; Wtac. by rewrite (in_graph_Vf fg xg) -(e2 _ Pg); Wtac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)