proposition: Lemma eqvars_remove_nvar : forall vars1 vars2 v, eqvars vars1 vars2 -> eqvars (remove_nvar vars1 v) (remove_nvar vars2 v).
proof: Proof. introv. trw eqvars_prop. allrw eqvars_prop; sp. allrw in_remove_nvar. allrw; sp. Qed.
imports: list Omega