proposition: Lemma subvars_cons_r_weak_if_not_in : forall vs1 v vs2, subvars vs1 (v :: vs2) -> !LIn v vs1 -> subvars vs1 vs2.
proof: Proof. introv sv ni. allrw subvars_prop. introv i. applydup sv in i as j. allsimpl; sp; subst; sp. Qed.
imports: list Omega