proposition: Lemma disjoint_remove_nvars2: forall lva lvb lvc, disjoint lvb lva -> disjoint (remove_nvars lvc lvb) lva.
proof: Proof. introv Hin Hc. apply in_remove_nvars in Hc. exrepnd. introv Hinc. disjoint_lin_contra. Qed.
imports: list Omega