proposition: Lemma function_exten3 f g: function f -> function g -> graph f = graph g -> target f = target g -> source f = source g -> f = g.
proof: Proof. move => [[ff _] _ _] [[fg _] _ _] e1 e2 e3. by rewrite -(corresp_recov ff) -(corresp_recov fg); congr (triple _ _ _). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)