proposition: Lemma ALFilterAppAsDiff : forall sub l1 l2, ALFilter sub (l1 ++ l2) = ALFilter sub (l1 ++ diff DeqKey l1 l2).
proof: Proof. induction sub; simpl; sp; allsimpl;[]. cases_ifd Hd; cases_ifd Hdd; cpx; allrw in_app_iff; allrw in_diff. - provefalse. apply Hddf. dorn Hdt; cpx;[]. pose proof (in_deq _ DeqKey a0 l1) as X. dorn X; cpx. - provefalse. apply Hdf. dorn Hddt; exrepnd; cpx. - f_equal. auto. Qed.
imports: list Omega