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