val filter_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a)
    : Tot (m: list a {forall x. memP x m ==> f env x})
val filter_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a)
    : Tot (m: list a {forall x. memP x m ==> f env x})
let rec filter_aux (#a:Type)
                   (#b:Type)
                   (env:b)
                   (f:(b -> a -> Tot bool))
                   (l: list a)
    : Tot (m:list a{forall x. memP x m ==> f env x}) =
      match l with
      | [] -> []
      | hd::tl -> if f env hd then hd::filter_aux env f tl else filter_aux env f tl
module MiTLS.List.Helpers
open MiTLS

open FStar.List.Tot

(* Some basic utility functions for closure converting arguments
   to the higher-order combinators in the list library ...
/
prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked
MiTLS.List.Helpers.fst
env: b -> f: (_: b -> _: a -> Prims.bool) -> l: Prims.list a
  -> m: Prims.list a {forall (x: a). FStar.List.Tot.Base.memP x m ==> f env x}
Prims.bool Prims.list Prims.Nil Prims.Cons MiTLS.List.Helpers.filter_aux Prims.l_Forall Prims.l_imp FStar.List.Tot.Base.memP Prims.b2t
let rec filter_aux (#a #b: Type) (env: b) (f: (b -> a -> Tot bool)) (l: list a)
    : Tot (m: list a {forall x. memP x m ==> f env x}) =
  
match l with
| [] -> []
| hd :: tl -> if f env hd then hd :: filter_aux env f tl else filter_aux env f tl