proposition: Lemma unC2 h1 h2 : h1 :++ h2 = h2 :++ h1.
proof: Proof. by congr (_, _); rewrite unC. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep