proposition: Lemma term_uniq x y z : functional -> terminal y -> terminal z -> connect e x y -> connect e x z -> y = z.
proof: Proof. move => fun_e Ty Tz /connectP [p] p1 p2 /connectP [q]. elim: p q x p1 p2 => [|a p IH] [|b q] x /=; first congruence. - move => _ <-. by rewrite Ty. - case/andP => xa _ _ _ H. by rewrite -H Tz in xa. - case/andP => xa p1 p2 /andP [xb] q1 q2. move: (fun_e _ _ _ xa xb) => ?; subst b. exact: IH q2. Qed.
imports: mathcomp(all_ssreflect)