proposition: Lemma merge_path x s1 s2 : path leT x s1 -> path leT x s2 -> path leT x (merge s1 s2).
proof: Proof. by rewrite !(eq_path leElex); apply/merge_stable_path/allrelT. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)