proposition: Lemma eqUh h1 h2 h : def (h1 :+ h) -> h1 :+ h = h2 :+ h -> def h1 /\ h1 = h2.
proof: Proof. by move=>D E; rewrite {2}(unKhl D E) (defUnl D). Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep