proposition: Lemma ALFilterLIn : forall v t sub vars, LIn (v, t) (ALFilter sub vars) <=> ( LIn (v, t) sub # ! LIn v vars ).
proof: Proof. induction sub; simpl; sp. split; sp. cases_if; simpl; allrw; split; sp; cpx. contradiction. Qed.
imports: list Omega