proposition: Lemma un0h2 h : (empty, empty) :++ h = h.
proof: Proof. by case: h=>h1 h2; rewrite /plus2 /= !un0h. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep