proposition: Lemma subvars_comm_r : forall vs vs1 vs2, subvars vs (vs1 ++ vs2) <=> subvars vs (vs2 ++ vs1).
proof: Proof. introv. trw subvars_prop. alltrewrite subvars_prop; split; introv Hyp Hin; apply Hyp in Hin; alltrewrite in_app_iff; sp; auto. Qed.
imports: list Omega