proposition: Lemma ALFilterDom : forall sub lv, ALFilter sub (lv++ALDom sub) =[].
proof: Proof. induction sub as [|(v,u) sub Hind] ; introv ; auto;[]. allsimpl. cases_ifd Hd; cpx; allsimpl; allrw in_app_iff; cpx. - rw cons_as_app. rw app_assoc. rw Hind; auto. - provefalse. apply Hdf. right. cpx. Qed.
imports: list Omega