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