proposition: Lemma left_pf x (h : heap) (f : find x) : invariant x (left_tag (untag (heap_of f) :+ h)).
proof: Proof. case:f=>[[i]]; rewrite /invariant /= => H D. by rewrite domUn !inE /= D (H (defUnl D)). Qed.
imports: mathcomp(ssreflect ssrbool ssrnat eqtype) LemmaOverloading(heaps)