proposition: Lemma subvars_eqvars : forall s1 s2 s3, subvars s1 s2 -> eqvars s1 s3 -> subvars s3 s2.
proof: Proof. introv s e. allrw subvars_prop. allrw eqvars_prop. introv i. apply e in i. apply s in i; auto. Qed.
imports: list Omega