proposition: Lemma eqvars_disjoint_r: forall s s1 s2 : list NVar, eqvars s1 s2 -> disjoint s s1 -> disjoint s s2.
proof: Proof. unfold disjoint. introv eqv disj i k. rw eqvars_prop in eqv. applydup disj in i as j. apply eqv in k; sp. Qed.
imports: list Omega