proposition: Lemma ALFilterSwap : forall l1 l2 sub, ALFilter (ALFilter sub l1) l2 = ALFilter (ALFilter sub l2) l1.
proof: Proof. induction sub; simpl; sp. allsimpl; cases_if as H1d; cases_if as H2d; allsimpl; try (rw H1d); try (rw H2d); cpx; try (rw IHsub); cpx. Qed.
imports: list Omega