proposition: Lemma subvars_remove_nvars : forall vs1 vs2 vs3, subvars (remove_nvars vs1 vs2) vs3 <=> subvars vs2 (vs3 ++ vs1).
proof: Proof. sp; repeat (trw subvars_eq); unfold remove_nvars. trw subset_diff; sp. Qed.
imports: list Omega