proposition: Lemma eqvars_remove_nvars_implies : forall vs1 vs2 vs3, eqvars vs1 (remove_nvars vs2 vs3) -> disjoint vs1 vs2 # subvars vs1 vs3.
proof: Proof. introv eqv. allrw eqvars_prop. unfold disjoint. rw subvars_prop; dands; introv i; apply eqv in i; rw in_remove_nvars in i; sp. Qed.
imports: list Omega