proposition: Lemma function_exten1 f g: function f -> function g -> graph f = graph g -> target f = target g -> f = g.
proof: Proof. move => ff fg e1 e2; apply: function_exten3=>//. by rewrite -!domain_fg // e1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)