proposition: Lemma function_exten5 x y a b: inc a (functions x y) -> inc b (functions x y) -> graph a = graph b -> a = b.
proof: Proof. move /functionsP=> [fa sa ta] /functionsP [fb sb tb] sg. apply: function_exten1=>//; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)