proposition: Lemma eqvars_disjoint : forall s1 s2 s3, eqvars s1 s2 -> disjoint s1 s3 -> disjoint s2 s3.
proof: Proof. introv eqv disj. unfold disjoint. unfold disjoint in disj. introv i. rw eqvars_prop in eqv. apply eqv in i. apply disj in i; sp. Qed.
imports: list Omega