proposition: Lemma un0E h1 h2 : h1 :+ h2 = empty <-> h1 = empty /\ h2 = empty.
proof: Proof. by rewrite !empbE empUn; case: andP. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep