proposition: Lemma filter_eq : forall A (p:A->bool) (P:A->Prop) l, isTrue_pred p P -> filter p l = LibList.filter P l.
proof: Proof. Proof using. Local Transparent LibList.filter. introv E. unfold filter, LibList.filter. rew_list_exec. fequals. extens. intros. rewrite E. rewrite* if_isTrue. Qed.
imports: TLC(LibTactics LibReflect)