proposition: Lemma var_pf keys vars1 vars2 n (f : xfind vars1 vars2 n) : axiom (Context keys vars1) (Context keys vars2) [:: Var T n] (var_tag (xuntag f)).
proof: Proof. by case: f=>p [E H]; split=>//=; rewrite ?E ?unitR // (onth_size E). Qed.
imports: Coq(ssreflect ssrbool ssrfun) mathcomp(ssrnat eqtype seq) pcm(options pred prelude) pcm(pcm unionmap natmap)