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