open Preamble

open Div_and_mod

open Jmeq

open Russell

open Bool

open Relations

open Nat

open Hints_declaration

open Core_notation

open Pts

open Logic

open Types

open List

open Util

(** val foldl_strong_internal :
    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
let rec foldl_strong_internal l h prefix suffix acc =
  (match suffix with
   | List.Nil ->
     (fun _ -> Util.eq_rect_Type0_r prefix acc (List.append prefix List.Nil))
   | List.Cons (hd, tl) ->
     (fun _ ->
       Logic.eq_coerc
         (foldl_strong_internal l h
           (List.append prefix (List.Cons (hd, List.Nil))) tl
           (h prefix hd tl __ acc)))) __

(** val foldl_strong :
    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
    'a2) -> 'a2 -> 'a2 **)
let foldl_strong l h acc =
  foldl_strong_internal l h List.Nil l acc

(** val foldr_strong_internal :
    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
    'a2) -> 'a1 List.list -> 'a1 List.list -> 'a2 -> 'a2 **)
let rec foldr_strong_internal l h prefix suffix acc =
  (match suffix with
   | List.Nil -> (fun _ -> acc)
   | List.Cons (hd, tl) ->
     (fun _ ->
       h prefix hd tl __
         (foldr_strong_internal l h
           (List.append prefix (List.Cons (hd, List.Nil))) tl acc))) __

(** val foldr_strong :
    'a1 List.list -> ('a1 List.list -> 'a1 -> 'a1 List.list -> __ -> 'a2 ->
    'a2) -> 'a2 -> 'a2 **)
let foldr_strong l h acc =
  foldr_strong_internal l h List.Nil l acc