proposition: Lemma var_pf hs1 hs2 xs n (f : xfind hs1 hs2 n) : invariant (Context hs1 xs) (Context hs2 xs) [:: Var n] (var_tag (xuntag f)).
proof: Proof. case:f=>p [H1 H2]; split; first by rewrite /= /hlook H1. - by split; [|apply: prefix_refl]. by apply/andP; rewrite /= (onth_size H1). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool ssrnat seq eqtype) LemmaOverloading(prelude prefix xfind heaps terms)