proposition: Lemma subdom_emp_inv h : subdom h empty -> h = empty.
proof: Proof. case: h=>[|h H] //; rewrite /subdom /=. case: (allP (s:=supp h))=>// E _; apply/heapE; apply: fmapP=>x. case: suppP (E x)=>// v E2; move/(_ (erefl _)). by rewrite supp_nil. Qed.
imports: mathcomp(ssreflect ssrfun ssrnat div ssrbool seq) LemmaOverloading(prelude finmap ordtype) mathcomp(path eqtype) Eqdep