proposition: Lemma allrel_merge s1 s2 : allrel leT s1 s2 -> merge s1 s2 = s1 ++ s2.
proof: Proof. elim: s1 s2 => [|x s1 IHs1] [|y s2]; rewrite ?cats0 //=. by rewrite allrel_consl /= -andbA => /and3P [-> _ /IHs1->]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq)