proposition: Lemma empty_pf i : invariant i i [::] (empty_tag empty).
proof: Proof. split; by [|apply: subctx_refl|]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)