proposition: Lemma subvars_disjoint_l : forall (l1 l2 l3 : list NVar), subvars l1 l2 -> disjoint l2 l3 -> disjoint l1 l3.
proof: Proof. introv. rw subvars_eq. pose proof (subset_disjoint NVar l1 l2 l3); sp. Qed.
imports: list Omega