proposition: Lemma exit2 h1 h : def (h1 :+ h) -> h1 :+ h = h -> def h1 /\ h1 = empty.
proof: Proof. by move=>H1; rewrite -{2}(unh0 h)=>H2; apply: exit1 H2. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep