proposition: Lemma filter_empty: forall A B {IB:Inhab B} (f:A->B->Prop), filter f empty = empty.
proof: Proof. Proof using . intros. applys filter_none. intros x K. rewrite* indom_empty_eq in K. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibOption LibRelation LibLogic LibOperation LibEpsilon LibMonoid LibSet)