cleanup: update F*, remove for_allP

Author: TWal

flake.lock

@@ -2,13 +2,6 @@ module Comparse.Parser.Builtins
 
 #set-options "--fuel 0 --ifuel 2"
 
-#push-options "--fuel 1"
-let rec for_allP_eq #a pre l =
-  match l with
-  | [] -> ()
-  | h::t -> for_allP_eq pre t
-#pop-options
-
 let is_not_unit #bytes #bl #a ps_a = forall (x:a). 1 <= prefixes_length (ps_a.serialize x)
 
 let is_well_formed_prefix_weaken #bytes #bl #a ps_a pre_strong pre_weak x =

src/Comparse.Parser.Builtins.fst

@@ -109,14 +109,6 @@ noeq type parser_serializer_prefix (bytes:Type0) {|bytes_like bytes|} (a:Type) =
 ///
 /// -- End parenthesis about symbolic bytes --
 
-let rec for_allP (#a:Type) (pre:a -> prop) (l:list a): prop =
-    match l with
-    | [] -> True
-    | h::t -> pre h /\ for_allP pre t
-
-val for_allP_eq: #a:Type -> pre:(a -> prop) -> l:list a ->
-  Lemma (for_allP pre l <==> (forall x. List.Tot.memP x l ==> pre x))
-
 [@@"opaque_to_smt"]
 let prefixes_length (#bytes:Type) {|bytes_like bytes|} (l:list bytes) =
   let add (x:nat) (y:nat): nat = x+y in