proposition: Lemma subvars_disjoint_r : forall l1 l2 l3 : list NVar, subvars l1 l2 -> disjoint l3 l2 -> disjoint l3 l1.
proof: Proof. introv sv disj. allrw subvars_prop. introv i j. apply sv in j. apply disj in i; sp. Qed.
imports: list Omega