proposition: Lemma ALFilterAppR : forall sub vs1 vs2, ALFilter sub (vs1 ++ vs2) = ALFilter (ALFilter sub vs1) vs2.
proof: Proof. induction sub; simpl; sp. rw <- memberb_din. rw <- memberb_din. rw memberb_app. destructr (memberb DeqKey a0 vs1) as [m1 | m1]; simpl. apply IHsub. rw <- memberb_din. allsimpl. destruct (memberb DeqKey a0 vs2) as [m2 | m2]; simpl; subst; try(rw IHsub); auto. Qed.
imports: list Omega