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