proposition: Lemma subvars_swap_r : forall vs1 vs2 vs, subvars vs (vs1 ++ vs2) <=> subvars vs (vs2 ++ vs1).
proof: Proof. sp; alltrewrite subvars_eq; unfold subset; split; sp; alltrewrite in_app_iff; apply_in_hyp p; allrw in_app_iff; sp. Qed.
imports: list Omega