Library CFML.Stdlib.List_ml

Set Implicit Arguments.

Require Coq.ZArith.BinInt TLC.LibLogic TLC.LibRelation TLC.LibInt TLC.LibListZ CFML.Shared CFML.CFHeaps CFML.CFApp CFML.CFPrint CFML.CFBuiltin.

Require Import Coq.ZArith.BinIntDef CFML.CFHeader.

Delimit Scope Z_scope with Z.

Local Open Scope cfheader_scope.

Parameter length : CFML.CFApp.func.

Parameter length__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat length) (
        forall A_ : Type,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                forall B_ : Type,
                forall len : Coq.ZArith.BinInt.Z,
                forall x0__ : Coq.Init.Datatypes.list B_,
                forall H : CFML.CFHeaps.hprop,
                forall Q : Coq.ZArith.BinInt.Z -> CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              TLC.LibLogic.pred_incl H (Q len)
                            )
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall a : B_,
                                forall l : Coq.Init.Datatypes.list B_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                  @CFML.CFApp.app_def aux (
                                    Coq.Lists.List.cons (
                                      @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                        Coq.ZArith.BinInt.Z.add len (1)%Z
                                      )
                                    ) (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn (
                                          Coq.Init.Datatypes.list B_
                                        ) l
                                      ) Coq.Lists.List.nil
                                    )
                                  ) Coq.ZArith.BinInt.Z
                                ) H Q
                              ) (
                                (
                                  forall a : B_,
                                  forall l : Coq.Init.Datatypes.list B_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z len
                  ) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) x0__
                    ) Coq.Lists.List.nil
                  )
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (0)%Z
                ) (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                  ) Coq.Lists.List.nil
                )
              ) Coq.ZArith.BinInt.Z
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def length (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l) Coq.Lists.List.nil
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF length) => CFHeader_Provide length__cf.

Parameter nth : CFML.CFApp.func.

Parameter nth__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat nth) (
        forall A_ : Type,
        forall l : Coq.Init.Datatypes.list A_,
        forall n : Coq.ZArith.BinInt.Z,
        forall H : CFML.CFHeaps.hprop,
        forall Q : A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_seq (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            Coq.Init.Logic.ex (
              fun Q' : _ -> CFML.CFHeaps.hprop =>
              Coq.Init.Logic.and (
                CFML.CFPrint.tag CFML.CFPrint.tag_assert (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (
                            Q (
                              (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) n (
                                0
                              )%Z
                            )
                          )
                        )
                      ) H (
                        fun _b : Coq.Init.Datatypes.bool =>
                        CFML.CFHeaps.heap_is_star (
                          CFML.CFHeaps.heap_is_empty_st (
                            Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
                          )
                        ) H
                      )
                    ) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
                  )
                ) H Q'
              ) (
                CFML.CFPrint.tag CFML.CFPrint.tag_fun (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    forall aux : CFML.CFApp.func,
                    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
                      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                        forall B_ : Type,
                        forall l : Coq.Init.Datatypes.list B_,
                        forall n : Coq.ZArith.BinInt.Z,
                        forall H : CFML.CFHeaps.hprop,
                        forall Q : B_ -> CFML.CFHeaps.hprop,
                        CFML.CFPrint.tag CFML.CFPrint.tag_val (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            forall x0__ : Coq.Init.Datatypes.list B_,
                            Coq.Init.Logic.eq x0__ l ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_match (
                              CFML.CFHeaps.local (
                                CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.and (
                                      Coq.Init.Logic.eq x0__ (
                                        Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                      ) ->
                                      CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          Coq.Init.Logic.False
                                        )
                                      ) H Q
                                    ) (
                                      Coq.Init.Logic.not (
                                        Coq.Init.Logic.eq x0__ (
                                          Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                        )
                                      ) ->
                                      CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          Coq.Init.Logic.and (
                                            forall a : B_,
                                            forall l :
                                              Coq.Init.Datatypes.list B_,
                                            Coq.Init.Logic.eq x0__ (
                                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                            ) ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                              CFML.CFHeaps.local (
                                                CFML.CFPrint.cf_let (
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      TLC.LibLogic.pred_incl H (
                                                        Q (
                                                          (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
                                                            0
                                                          )%Z
                                                        )
                                                      )
                                                    )
                                                  )
                                                ) (
                                                  fun x1__ :
                                                    Coq.Init.Datatypes.bool
                                                  =>
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.and (
                                                        Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.true ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                                          CFML.CFHeaps.local (
                                                            fun H :
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            fun Q :
                                                              _ ->
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            TLC.LibLogic.pred_incl H (
                                                              Q a
                                                            )
                                                          )
                                                        ) H Q
                                                      ) (
                                                        Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.false ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                                          @CFML.CFApp.app_def aux (
                                                            Coq.Lists.List.cons (
                                                              @CFML.CFHeaps.dyn (
                                                                Coq.Init.Datatypes.list B_
                                                              ) l
                                                            ) (
                                                              Coq.Lists.List.cons (
                                                                @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                                  Coq.ZArith.BinInt.Z.sub n (
                                                                    1
                                                                  )%Z
                                                                )
                                                              ) Coq.Lists.List.nil
                                                            )
                                                          ) B_
                                                        ) H Q
                                                      )
                                                    )
                                                  )
                                                )
                                              )
                                            ) H Q
                                          ) (
                                            (
                                              forall a : B_,
                                              forall l :
                                                Coq.Init.Datatypes.list B_,
                                              Coq.Init.Logic.not (
                                                Coq.Init.Logic.eq x0__ (
                                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                )
                                              )
                                            ) ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                              CFML.CFHeaps.local (
                                                fun H : CFML.CFHeaps.hprop =>
                                                fun Q :
                                                  _ -> CFML.CFHeaps.hprop
                                                =>
                                                Coq.Init.Logic.True
                                              )
                                            ) H Q
                                          )
                                        )
                                      ) H Q
                                    )
                                  )
                                )
                              )
                            ) H Q
                          )
                        ) H Q ->
                        CFML.CFApp.app_def aux (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l
                          ) (
                            Coq.Lists.List.cons (
                              @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                            ) Coq.Lists.List.nil
                          )
                        ) H Q
                      )
                    ) ->
                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                      @CFML.CFApp.app_def aux (
                        Coq.Lists.List.cons (
                          @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                        ) (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                          ) Coq.Lists.List.nil
                        )
                      ) A_
                    ) H Q
                  )
                ) (Q' Coq.Init.Datatypes.tt) Q
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def nth (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l) (
            Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF nth) => CFHeader_Provide nth__cf.

Parameter append : CFML.CFApp.func.

Parameter append__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat append) (
        forall A_ : Type,
        forall l1 : Coq.Init.Datatypes.list A_,
        forall l2 : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat aux) (
                forall x0__ : Coq.Init.Datatypes.list A_,
                forall H : CFML.CFHeaps.hprop,
                forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              TLC.LibLogic.pred_incl H (Q l2)
                            )
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall a : A_,
                                forall l : Coq.Init.Datatypes.list A_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                  CFML.CFHeaps.local (
                                    CFML.CFPrint.cf_let (
                                      CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                        @CFML.CFApp.app_def aux (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        ) (Coq.Init.Datatypes.list A_)
                                      )
                                    ) (
                                      fun x1__ : Coq.Init.Datatypes.list A_ =>
                                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          TLC.LibLogic.pred_incl H (
                                            Q (
                                              Coq.Lists.List.cons a x1__ : Coq.Init.Datatypes.list A_
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                ) H Q
                              ) (
                                (
                                  forall a : A_,
                                  forall l : Coq.Init.Datatypes.list A_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
                  ) Coq.Lists.List.nil
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
                ) Coq.Lists.List.nil
              ) (Coq.Init.Datatypes.list A_)
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def append (
          Coq.Lists.List.cons (
            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
          ) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l2
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF append) => CFHeader_Provide append__cf.

Parameter infix_at__ : CFML.CFApp.func.

Parameter infix_at____cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_val (
    Coq.Init.Logic.eq infix_at__ (append : CFML.CFApp.func)
  ).

Hint Extern 1 (RegisterCF infix_at__) => CFHeader_Provide infix_at____cf.

Parameter rev_append : CFML.CFApp.func.

Parameter rev_append__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat rev_append) (
        forall A_ : Type,
        forall l1 : Coq.Init.Datatypes.list A_,
        forall l2 : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq l1 (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (Q l2)
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq l1 (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq l1 (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                          @CFML.CFApp.app_def rev_append (
                            Coq.Lists.List.cons (
                              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                            ) (
                              Coq.Lists.List.cons (
                                @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
                                  Coq.Lists.List.cons a l2 : Coq.Init.Datatypes.list A_
                                )
                              ) Coq.Lists.List.nil
                            )
                          ) (Coq.Init.Datatypes.list A_)
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq l1 (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def rev_append (
          Coq.Lists.List.cons (
            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
          ) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l2
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF rev_append) => CFHeader_Provide rev_append__cf.

Parameter rev : CFML.CFApp.func.

Parameter rev__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat rev) (
        forall A_ : Type,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
          @CFML.CFApp.app_def rev_append (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) (
              Coq.Lists.List.cons (
                @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
                  Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                )
              ) Coq.Lists.List.nil
            )
          ) (Coq.Init.Datatypes.list A_)
        ) H Q ->
        CFML.CFApp.app_def rev (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l) Coq.Lists.List.nil
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF rev) => CFHeader_Provide rev__cf.

Parameter concat : CFML.CFApp.func.

Parameter concat__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat concat) (
        forall A_ : Type,
        forall x0__ : Coq.Init.Datatypes.list (Coq.Init.Datatypes.list A_),
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list (
                        Coq.Init.Datatypes.list A_
                      )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (Coq.Lists.List.nil : Coq.Init.Datatypes.list A_)
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list (
                          Coq.Init.Datatypes.list A_
                        )
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall l : Coq.Init.Datatypes.list A_,
                        forall r :
                          Coq.Init.Datatypes.list (Coq.Init.Datatypes.list A_),
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons l r : Coq.Init.Datatypes.list (
                              Coq.Init.Datatypes.list A_
                            )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def concat (
                                  Coq.Lists.List.cons (
                                    @CFML.CFHeaps.dyn (
                                      Coq.Init.Datatypes.list (
                                        Coq.Init.Datatypes.list A_
                                      )
                                    ) r
                                  ) Coq.Lists.List.nil
                                ) (Coq.Init.Datatypes.list A_)
                              )
                            ) (
                              fun x1__ : Coq.Init.Datatypes.list A_ =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def infix_at__ (
                                  Coq.Lists.List.cons (
                                    @CFML.CFHeaps.dyn (
                                      Coq.Init.Datatypes.list A_
                                    ) l
                                  ) (
                                    Coq.Lists.List.cons (
                                      @CFML.CFHeaps.dyn (
                                        Coq.Init.Datatypes.list A_
                                      ) x1__
                                    ) Coq.Lists.List.nil
                                  )
                                ) (Coq.Init.Datatypes.list A_)
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall l : Coq.Init.Datatypes.list A_,
                          forall r :
                            Coq.Init.Datatypes.list (Coq.Init.Datatypes.list A_),
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons l r : Coq.Init.Datatypes.list (
                                  Coq.Init.Datatypes.list A_
                                )
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def concat (
          Coq.Lists.List.cons (
            @CFML.CFHeaps.dyn (
              Coq.Init.Datatypes.list (Coq.Init.Datatypes.list A_)
            ) x0__
          ) Coq.Lists.List.nil
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF concat) => CFHeader_Provide concat__cf.

Parameter iter : CFML.CFApp.func.

Parameter iter__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iter) (
        forall A_ : Type,
        forall f : CFML.CFApp.func,
        forall x0__ : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (Coq.Init.Datatypes.tt : Coq.Init.Datatypes.unit)
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_seq (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.ex (
                              fun Q' : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                  @CFML.CFApp.app_def f (
                                    Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ a) Coq.Lists.List.nil
                                  ) Coq.Init.Datatypes.unit
                                ) H Q'
                              ) (
                                CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                  @CFML.CFApp.app_def iter (
                                    Coq.Lists.List.cons (
                                      @CFML.CFHeaps.dyn CFML.CFApp.func f
                                    ) (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn (
                                          Coq.Init.Datatypes.list A_
                                        ) l
                                      ) Coq.Lists.List.nil
                                    )
                                  ) Coq.Init.Datatypes.unit
                                ) (Q' Coq.Init.Datatypes.tt) Q
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def iter (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF iter) => CFHeader_Provide iter__cf.

Parameter iteri : CFML.CFApp.func.

Parameter iteri__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat iteri) (
        forall A_ : Type,
        forall f : CFML.CFApp.func,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                forall i : Coq.ZArith.BinInt.Z,
                forall x0__ : Coq.Init.Datatypes.list A_,
                forall H : CFML.CFHeaps.hprop,
                forall Q : Coq.Init.Datatypes.unit -> CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              TLC.LibLogic.pred_incl H (
                                Q (
                                  Coq.Init.Datatypes.tt : Coq.Init.Datatypes.unit
                                )
                              )
                            )
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall a : A_,
                                forall l : Coq.Init.Datatypes.list A_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_seq (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.ex (
                                      fun Q' : _ -> CFML.CFHeaps.hprop =>
                                      Coq.Init.Logic.and (
                                        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                          @CFML.CFApp.app_def f (
                                            Coq.Lists.List.cons (
                                              @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
                                            ) (
                                              Coq.Lists.List.cons (
                                                @CFML.CFHeaps.dyn A_ a
                                              ) Coq.Lists.List.nil
                                            )
                                          ) Coq.Init.Datatypes.unit
                                        ) H Q'
                                      ) (
                                        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                          @CFML.CFApp.app_def aux (
                                            Coq.Lists.List.cons (
                                              @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                Coq.ZArith.BinInt.Z.add i (1)%Z
                                              )
                                            ) (
                                              Coq.Lists.List.cons (
                                                @CFML.CFHeaps.dyn (
                                                  Coq.Init.Datatypes.list A_
                                                ) l
                                              ) Coq.Lists.List.nil
                                            )
                                          ) Coq.Init.Datatypes.unit
                                        ) (Q' Coq.Init.Datatypes.tt) Q
                                      )
                                    )
                                  )
                                ) H Q
                              ) (
                                (
                                  forall a : A_,
                                  forall l : Coq.Init.Datatypes.list A_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
                    ) Coq.Lists.List.nil
                  )
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (0)%Z
                ) (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                  ) Coq.Lists.List.nil
                )
              ) Coq.Init.Datatypes.unit
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def iteri (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF iteri) => CFHeader_Provide iteri__cf.

Parameter map : CFML.CFApp.func.

Parameter map__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat map) (
        forall B_ : Type,
        forall A_ : Type,
        forall f : CFML.CFApp.func,
        forall x0__ : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list B_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (Coq.Lists.List.nil : Coq.Init.Datatypes.list B_)
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def f (
                                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ a) Coq.Lists.List.nil
                                ) B_
                              )
                            ) (
                              fun r : B_ =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                CFML.CFHeaps.local (
                                  CFML.CFPrint.cf_let (
                                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                      @CFML.CFApp.app_def map (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn CFML.CFApp.func f
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        )
                                      ) (Coq.Init.Datatypes.list B_)
                                    )
                                  ) (
                                    fun x1__ : Coq.Init.Datatypes.list B_ =>
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (
                                          Q (
                                            Coq.Lists.List.cons r x1__ : Coq.Init.Datatypes.list B_
                                          )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def map (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF map) => CFHeader_Provide map__cf.

Parameter mapi : CFML.CFApp.func.

Parameter mapi__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat mapi) (
        forall A_ : Type,
        forall B_ : Type,
        forall f : CFML.CFApp.func,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list B_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                forall i : Coq.ZArith.BinInt.Z,
                forall x0__ : Coq.Init.Datatypes.list A_,
                forall H : CFML.CFHeaps.hprop,
                forall Q : Coq.Init.Datatypes.list B_ -> CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              TLC.LibLogic.pred_incl H (
                                Q (
                                  Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                )
                              )
                            )
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall a : A_,
                                forall l : Coq.Init.Datatypes.list A_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                  CFML.CFHeaps.local (
                                    CFML.CFPrint.cf_let (
                                      CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                        @CFML.CFApp.app_def f (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i
                                          ) (
                                            Coq.Lists.List.cons (
                                              @CFML.CFHeaps.dyn A_ a
                                            ) Coq.Lists.List.nil
                                          )
                                        ) B_
                                      )
                                    ) (
                                      fun r : B_ =>
                                      CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                        CFML.CFHeaps.local (
                                          CFML.CFPrint.cf_let (
                                            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                              @CFML.CFApp.app_def aux (
                                                Coq.Lists.List.cons (
                                                  @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                    Coq.ZArith.BinInt.Z.add i (
                                                      1
                                                    )%Z
                                                  )
                                                ) (
                                                  Coq.Lists.List.cons (
                                                    @CFML.CFHeaps.dyn (
                                                      Coq.Init.Datatypes.list A_
                                                    ) l
                                                  ) Coq.Lists.List.nil
                                                )
                                              ) (Coq.Init.Datatypes.list B_)
                                            )
                                          ) (
                                            fun x1__ :
                                              Coq.Init.Datatypes.list B_
                                            =>
                                            CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                              CFML.CFHeaps.local (
                                                fun H : CFML.CFHeaps.hprop =>
                                                fun Q :
                                                  _ -> CFML.CFHeaps.hprop
                                                =>
                                                TLC.LibLogic.pred_incl H (
                                                  Q (
                                                    Coq.Lists.List.cons r x1__ : Coq.Init.Datatypes.list B_
                                                  )
                                                )
                                              )
                                            )
                                          )
                                        )
                                      )
                                    )
                                  )
                                ) H Q
                              ) (
                                (
                                  forall a : A_,
                                  forall l : Coq.Init.Datatypes.list A_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z i) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
                    ) Coq.Lists.List.nil
                  )
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (0)%Z
                ) (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                  ) Coq.Lists.List.nil
                )
              ) (Coq.Init.Datatypes.list B_)
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def mapi (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF mapi) => CFHeader_Provide mapi__cf.

Parameter fold_left : CFML.CFApp.func.

Parameter fold_left__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_left) (
        forall A_ : Type,
        forall B_ : Type,
        forall f : CFML.CFApp.func,
        forall acc : A_,
        forall l : Coq.Init.Datatypes.list B_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_val (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall x0__ : Coq.Init.Datatypes.list B_,
            Coq.Init.Logic.eq x0__ l ->
            CFML.CFPrint.tag CFML.CFPrint.tag_match (
              CFML.CFHeaps.local (
                CFML.CFPrint.tag CFML.CFPrint.tag_case (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      Coq.Init.Logic.eq x0__ (
                        Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (Q acc)
                        )
                      ) H Q
                    ) (
                      Coq.Init.Logic.not (
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                        )
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_case (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          Coq.Init.Logic.and (
                            forall a : B_,
                            forall l : Coq.Init.Datatypes.list B_,
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_let (
                              CFML.CFHeaps.local (
                                CFML.CFPrint.cf_let (
                                  CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                    @CFML.CFApp.app_def f (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn A_ acc
                                      ) (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn B_ a
                                        ) Coq.Lists.List.nil
                                      )
                                    ) A_
                                  )
                                ) (
                                  fun x1__ : A_ =>
                                  CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                    @CFML.CFApp.app_def fold_left (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn CFML.CFApp.func f
                                      ) (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn A_ x1__
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list B_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        )
                                      )
                                    ) A_
                                  )
                                )
                              )
                            ) H Q
                          ) (
                            (
                              forall a : B_,
                              forall l : Coq.Init.Datatypes.list B_,
                              Coq.Init.Logic.not (
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                )
                              )
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_done (
                              CFML.CFHeaps.local (
                                fun H : CFML.CFHeaps.hprop =>
                                fun Q : _ -> CFML.CFHeaps.hprop =>
                                Coq.Init.Logic.True
                              )
                            ) H Q
                          )
                        )
                      ) H Q
                    )
                  )
                )
              )
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def fold_left (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ acc) (
              Coq.Lists.List.cons (
                @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l
              ) Coq.Lists.List.nil
            )
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF fold_left) => CFHeader_Provide fold_left__cf.

Parameter fold_right : CFML.CFApp.func.

Parameter fold_right__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat fold_right) (
        forall B_ : Type,
        forall A_ : Type,
        forall f : CFML.CFApp.func,
        forall l : Coq.Init.Datatypes.list A_,
        forall acc : B_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : B_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_val (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall x0__ : Coq.Init.Datatypes.list A_,
            Coq.Init.Logic.eq x0__ l ->
            CFML.CFPrint.tag CFML.CFPrint.tag_match (
              CFML.CFHeaps.local (
                CFML.CFPrint.tag CFML.CFPrint.tag_case (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      Coq.Init.Logic.eq x0__ (
                        Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (Q acc)
                        )
                      ) H Q
                    ) (
                      Coq.Init.Logic.not (
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                        )
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_case (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          Coq.Init.Logic.and (
                            forall a : A_,
                            forall l : Coq.Init.Datatypes.list A_,
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_let (
                              CFML.CFHeaps.local (
                                CFML.CFPrint.cf_let (
                                  CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                    @CFML.CFApp.app_def fold_right (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn CFML.CFApp.func f
                                      ) (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn (
                                            Coq.Init.Datatypes.list A_
                                          ) l
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn B_ acc
                                          ) Coq.Lists.List.nil
                                        )
                                      )
                                    ) B_
                                  )
                                ) (
                                  fun x1__ : B_ =>
                                  CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                    @CFML.CFApp.app_def f (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn A_ a
                                      ) (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn B_ x1__
                                        ) Coq.Lists.List.nil
                                      )
                                    ) B_
                                  )
                                )
                              )
                            ) H Q
                          ) (
                            (
                              forall a : A_,
                              forall l : Coq.Init.Datatypes.list A_,
                              Coq.Init.Logic.not (
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                )
                              )
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_done (
                              CFML.CFHeaps.local (
                                fun H : CFML.CFHeaps.hprop =>
                                fun Q : _ -> CFML.CFHeaps.hprop =>
                                Coq.Init.Logic.True
                              )
                            ) H Q
                          )
                        )
                      ) H Q
                    )
                  )
                )
              )
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def fold_right (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func f) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) (
              Coq.Lists.List.cons (@CFML.CFHeaps.dyn B_ acc) Coq.Lists.List.nil
            )
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF fold_right) => CFHeader_Provide fold_right__cf.

Parameter for_all : CFML.CFApp.func.

Parameter for_all__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat for_all) (
        forall A_ : Type,
        forall p : CFML.CFApp.func,
        forall x0__ : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool)
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def p (
                                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ a) Coq.Lists.List.nil
                                ) Coq.Init.Datatypes.bool
                              )
                            ) (
                              fun x1__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                      @CFML.CFApp.app_def for_all (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn CFML.CFApp.func p
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        )
                                      ) Coq.Init.Datatypes.bool
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (
                                          Q (
                                            Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool
                                          )
                                        )
                                      )
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def for_all (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func p) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF for_all) => CFHeader_Provide for_all__cf.

Parameter exists__ : CFML.CFApp.func.

Parameter exists____cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat exists__) (
        forall A_ : Type,
        forall p : CFML.CFApp.func,
        forall x0__ : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.bool -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (Coq.Init.Datatypes.false : Coq.Init.Datatypes.bool)
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def p (
                                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ a) Coq.Lists.List.nil
                                ) Coq.Init.Datatypes.bool
                              )
                            ) (
                              fun x1__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (
                                          Q (
                                            Coq.Init.Datatypes.true : Coq.Init.Datatypes.bool
                                          )
                                        )
                                      )
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                      @CFML.CFApp.app_def exists__ (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn CFML.CFApp.func p
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        )
                                      ) Coq.Init.Datatypes.bool
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def exists__ (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func p) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF exists__) => CFHeader_Provide exists____cf.

Parameter find : CFML.CFApp.func.

Parameter find__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat find) (
        forall A_ : Type,
        forall p : CFML.CFApp.func,
        forall x0__ : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.False
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall a : A_,
                        forall l : Coq.Init.Datatypes.list A_,
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def p (
                                  Coq.Lists.List.cons (@CFML.CFHeaps.dyn A_ a) Coq.Lists.List.nil
                                ) Coq.Init.Datatypes.bool
                              )
                            ) (
                              fun x1__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (Q a)
                                      )
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                      @CFML.CFApp.app_def find (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn CFML.CFApp.func p
                                        ) (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) l
                                          ) Coq.Lists.List.nil
                                        )
                                      ) A_
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall a : A_,
                          forall l : Coq.Init.Datatypes.list A_,
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def find (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func p) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF find) => CFHeader_Provide find__cf.

Parameter filter : CFML.CFApp.func.

Parameter filter__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat filter) (
        forall A_ : Type,
        forall p : CFML.CFApp.func,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                forall acc : Coq.Init.Datatypes.list A_,
                forall x0__ : Coq.Init.Datatypes.list A_,
                forall H : CFML.CFHeaps.hprop,
                forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                            @CFML.CFApp.app_def rev (
                              Coq.Lists.List.cons (
                                @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) acc
                              ) Coq.Lists.List.nil
                            ) (Coq.Init.Datatypes.list A_)
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall a : A_,
                                forall l : Coq.Init.Datatypes.list A_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                  CFML.CFHeaps.local (
                                    CFML.CFPrint.cf_let (
                                      CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                        @CFML.CFApp.app_def p (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn A_ a
                                          ) Coq.Lists.List.nil
                                        ) Coq.Init.Datatypes.bool
                                      )
                                    ) (
                                      fun x1__ : Coq.Init.Datatypes.bool =>
                                      CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          Coq.Init.Logic.and (
                                            Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.true ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                              @CFML.CFApp.app_def aux (
                                                Coq.Lists.List.cons (
                                                  @CFML.CFHeaps.dyn (
                                                    Coq.Init.Datatypes.list A_
                                                  ) (
                                                    Coq.Lists.List.cons a acc : Coq.Init.Datatypes.list A_
                                                  )
                                                ) (
                                                  Coq.Lists.List.cons (
                                                    @CFML.CFHeaps.dyn (
                                                      Coq.Init.Datatypes.list A_
                                                    ) l
                                                  ) Coq.Lists.List.nil
                                                )
                                              ) (Coq.Init.Datatypes.list A_)
                                            ) H Q
                                          ) (
                                            Coq.Init.Logic.eq x1__ Coq.Init.Datatypes.false ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                              @CFML.CFApp.app_def aux (
                                                Coq.Lists.List.cons (
                                                  @CFML.CFHeaps.dyn (
                                                    Coq.Init.Datatypes.list A_
                                                  ) acc
                                                ) (
                                                  Coq.Lists.List.cons (
                                                    @CFML.CFHeaps.dyn (
                                                      Coq.Init.Datatypes.list A_
                                                    ) l
                                                  ) Coq.Lists.List.nil
                                                )
                                              ) (Coq.Init.Datatypes.list A_)
                                            ) H Q
                                          )
                                        )
                                      )
                                    )
                                  )
                                ) H Q
                              ) (
                                (
                                  forall a : A_,
                                  forall l : Coq.Init.Datatypes.list A_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons a l : Coq.Init.Datatypes.list A_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) acc
                  ) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
                    ) Coq.Lists.List.nil
                  )
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  )
                ) (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                  ) Coq.Lists.List.nil
                )
              ) (Coq.Init.Datatypes.list A_)
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def filter (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func p) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF filter) => CFHeader_Provide filter__cf.

Parameter partition : CFML.CFApp.func.

Parameter partition__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat partition) (
        forall A_ : Type,
        forall p : CFML.CFApp.func,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q :
          Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
            Coq.Init.Datatypes.list A_
          ) ->
          CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_fun (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall aux : CFML.CFApp.func,
            CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
              Coq.Init.Logic.and (CFML.CFApp.curried (3)%nat aux) (
                forall yes : Coq.Init.Datatypes.list A_,
                forall no : Coq.Init.Datatypes.list A_,
                forall x0__ : Coq.Init.Datatypes.list A_,
                forall H : CFML.CFHeaps.hprop,
                forall Q :
                  Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
                    Coq.Init.Datatypes.list A_
                  ) ->
                  CFML.CFHeaps.hprop,
                CFML.CFPrint.tag CFML.CFPrint.tag_match (
                  CFML.CFHeaps.local (
                    CFML.CFPrint.tag CFML.CFPrint.tag_case (
                      CFML.CFHeaps.local (
                        fun H : CFML.CFHeaps.hprop =>
                        fun Q : _ -> CFML.CFHeaps.hprop =>
                        Coq.Init.Logic.and (
                          Coq.Init.Logic.eq x0__ (
                            Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_let (
                            CFML.CFHeaps.local (
                              CFML.CFPrint.cf_let (
                                CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                  @CFML.CFApp.app_def rev (
                                    Coq.Lists.List.cons (
                                      @CFML.CFHeaps.dyn (
                                        Coq.Init.Datatypes.list A_
                                      ) no
                                    ) Coq.Lists.List.nil
                                  ) (Coq.Init.Datatypes.list A_)
                                )
                              ) (
                                fun x2__ : Coq.Init.Datatypes.list A_ =>
                                CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                  CFML.CFHeaps.local (
                                    CFML.CFPrint.cf_let (
                                      CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                        @CFML.CFApp.app_def rev (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn (
                                              Coq.Init.Datatypes.list A_
                                            ) yes
                                          ) Coq.Lists.List.nil
                                        ) (Coq.Init.Datatypes.list A_)
                                      )
                                    ) (
                                      fun x1__ : Coq.Init.Datatypes.list A_ =>
                                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          TLC.LibLogic.pred_incl H (
                                            Q (x1__, x2__)
                                          )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          ) H Q
                        ) (
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                            )
                          ) ->
                          CFML.CFPrint.tag CFML.CFPrint.tag_case (
                            CFML.CFHeaps.local (
                              fun H : CFML.CFHeaps.hprop =>
                              fun Q : _ -> CFML.CFHeaps.hprop =>
                              Coq.Init.Logic.and (
                                forall x : A_,
                                forall l : Coq.Init.Datatypes.list A_,
                                Coq.Init.Logic.eq x0__ (
                                  Coq.Lists.List.cons x l : Coq.Init.Datatypes.list A_
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                  CFML.CFHeaps.local (
                                    CFML.CFPrint.cf_let (
                                      CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                        @CFML.CFApp.app_def p (
                                          Coq.Lists.List.cons (
                                            @CFML.CFHeaps.dyn A_ x
                                          ) Coq.Lists.List.nil
                                        ) Coq.Init.Datatypes.bool
                                      )
                                    ) (
                                      fun x3__ : Coq.Init.Datatypes.bool =>
                                      CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                        CFML.CFHeaps.local (
                                          fun H : CFML.CFHeaps.hprop =>
                                          fun Q : _ -> CFML.CFHeaps.hprop =>
                                          Coq.Init.Logic.and (
                                            Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.true ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                              @CFML.CFApp.app_def aux (
                                                Coq.Lists.List.cons (
                                                  @CFML.CFHeaps.dyn (
                                                    Coq.Init.Datatypes.list A_
                                                  ) (
                                                    Coq.Lists.List.cons x yes : Coq.Init.Datatypes.list A_
                                                  )
                                                ) (
                                                  Coq.Lists.List.cons (
                                                    @CFML.CFHeaps.dyn (
                                                      Coq.Init.Datatypes.list A_
                                                    ) no
                                                  ) (
                                                    Coq.Lists.List.cons (
                                                      @CFML.CFHeaps.dyn (
                                                        Coq.Init.Datatypes.list A_
                                                      ) l
                                                    ) Coq.Lists.List.nil
                                                  )
                                                )
                                              ) (
                                                Coq.Init.Datatypes.prod (
                                                  Coq.Init.Datatypes.list A_
                                                ) (Coq.Init.Datatypes.list A_)
                                              )
                                            ) H Q
                                          ) (
                                            Coq.Init.Logic.eq x3__ Coq.Init.Datatypes.false ->
                                            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                              @CFML.CFApp.app_def aux (
                                                Coq.Lists.List.cons (
                                                  @CFML.CFHeaps.dyn (
                                                    Coq.Init.Datatypes.list A_
                                                  ) yes
                                                ) (
                                                  Coq.Lists.List.cons (
                                                    @CFML.CFHeaps.dyn (
                                                      Coq.Init.Datatypes.list A_
                                                    ) (
                                                      Coq.Lists.List.cons x no : Coq.Init.Datatypes.list A_
                                                    )
                                                  ) (
                                                    Coq.Lists.List.cons (
                                                      @CFML.CFHeaps.dyn (
                                                        Coq.Init.Datatypes.list A_
                                                      ) l
                                                    ) Coq.Lists.List.nil
                                                  )
                                                )
                                              ) (
                                                Coq.Init.Datatypes.prod (
                                                  Coq.Init.Datatypes.list A_
                                                ) (Coq.Init.Datatypes.list A_)
                                              )
                                            ) H Q
                                          )
                                        )
                                      )
                                    )
                                  )
                                ) H Q
                              ) (
                                (
                                  forall x : A_,
                                  forall l : Coq.Init.Datatypes.list A_,
                                  Coq.Init.Logic.not (
                                    Coq.Init.Logic.eq x0__ (
                                      Coq.Lists.List.cons x l : Coq.Init.Datatypes.list A_
                                    )
                                  )
                                ) ->
                                CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                  CFML.CFHeaps.local (
                                    fun H : CFML.CFHeaps.hprop =>
                                    fun Q : _ -> CFML.CFHeaps.hprop =>
                                    Coq.Init.Logic.True
                                  )
                                ) H Q
                              )
                            )
                          ) H Q
                        )
                      )
                    )
                  )
                ) H Q ->
                CFML.CFApp.app_def aux (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) yes
                  ) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) no
                    ) (
                      Coq.Lists.List.cons (
                        @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) x0__
                      ) Coq.Lists.List.nil
                    )
                  )
                ) H Q
              )
            ) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_apply (
              @CFML.CFApp.app_def aux (
                Coq.Lists.List.cons (
                  @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                  )
                ) (
                  Coq.Lists.List.cons (
                    @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list A_
                    )
                  ) (
                    Coq.Lists.List.cons (
                      @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                    ) Coq.Lists.List.nil
                  )
                )
              ) (
                Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
                  Coq.Init.Datatypes.list A_
                )
              )
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def partition (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn CFML.CFApp.func p) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF partition) => CFHeader_Provide partition__cf.

Parameter split : CFML.CFApp.func.

Parameter split__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (1)%nat split) (
        forall B_ : Type,
        forall A_ : Type,
        forall x0__ : Coq.Init.Datatypes.list (Coq.Init.Datatypes.prod A_ B_),
        forall H : CFML.CFHeaps.hprop,
        forall Q :
          Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
            Coq.Init.Datatypes.list B_
          ) ->
          CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_match (
          CFML.CFHeaps.local (
            CFML.CFPrint.tag CFML.CFPrint.tag_case (
              CFML.CFHeaps.local (
                fun H : CFML.CFHeaps.hprop =>
                fun Q : _ -> CFML.CFHeaps.hprop =>
                Coq.Init.Logic.and (
                  Coq.Init.Logic.eq x0__ (
                    Coq.Lists.List.nil : Coq.Init.Datatypes.list (
                        Coq.Init.Datatypes.prod A_ B_
                      )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      TLC.LibLogic.pred_incl H (
                        Q (
                          (Coq.Lists.List.nil : Coq.Init.Datatypes.list A_),
                          (Coq.Lists.List.nil : Coq.Init.Datatypes.list B_)
                        )
                      )
                    )
                  ) H Q
                ) (
                  Coq.Init.Logic.not (
                    Coq.Init.Logic.eq x0__ (
                      Coq.Lists.List.nil : Coq.Init.Datatypes.list (
                          Coq.Init.Datatypes.prod A_ B_
                        )
                    )
                  ) ->
                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                    CFML.CFHeaps.local (
                      fun H : CFML.CFHeaps.hprop =>
                      fun Q : _ -> CFML.CFHeaps.hprop =>
                      Coq.Init.Logic.and (
                        forall x : A_,
                        forall y : B_,
                        forall l :
                          Coq.Init.Datatypes.list (
                            Coq.Init.Datatypes.prod A_ B_
                          ),
                        Coq.Init.Logic.eq x0__ (
                          Coq.Lists.List.cons (x, y) l : Coq.Init.Datatypes.list (
                              Coq.Init.Datatypes.prod A_ B_
                            )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                @CFML.CFApp.app_def split (
                                  Coq.Lists.List.cons (
                                    @CFML.CFHeaps.dyn (
                                      Coq.Init.Datatypes.list (
                                        Coq.Init.Datatypes.prod A_ B_
                                      )
                                    ) l
                                  ) Coq.Lists.List.nil
                                ) (
                                  Coq.Init.Datatypes.prod (
                                    Coq.Init.Datatypes.list A_
                                  ) (Coq.Init.Datatypes.list B_)
                                )
                              )
                            ) (
                              fun x1__ :
                                Coq.Init.Datatypes.prod (
                                  Coq.Init.Datatypes.list A_
                                ) (Coq.Init.Datatypes.list B_)
                              =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_match (
                                CFML.CFHeaps.local (
                                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                    CFML.CFHeaps.local (
                                      fun H : CFML.CFHeaps.hprop =>
                                      fun Q : _ -> CFML.CFHeaps.hprop =>
                                      Coq.Init.Logic.and (
                                        forall rx : Coq.Init.Datatypes.list A_,
                                        forall ry : Coq.Init.Datatypes.list B_,
                                        Coq.Init.Logic.eq x1__ (rx, ry) ->
                                        CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                          CFML.CFHeaps.local (
                                            fun H : CFML.CFHeaps.hprop =>
                                            fun Q : _ -> CFML.CFHeaps.hprop =>
                                            TLC.LibLogic.pred_incl H (
                                              Q (
                                                (
                                                  Coq.Lists.List.cons x rx : Coq.Init.Datatypes.list A_
                                                ),
                                                (
                                                  Coq.Lists.List.cons y ry : Coq.Init.Datatypes.list B_
                                                )
                                              )
                                            )
                                          )
                                        ) H Q
                                      ) (
                                        (
                                          forall rx :
                                            Coq.Init.Datatypes.list A_,
                                          forall ry :
                                            Coq.Init.Datatypes.list B_,
                                          Coq.Init.Logic.not (
                                            Coq.Init.Logic.eq x1__ (rx, ry)
                                          )
                                        ) ->
                                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                          CFML.CFHeaps.local (
                                            fun H : CFML.CFHeaps.hprop =>
                                            fun Q : _ -> CFML.CFHeaps.hprop =>
                                            Coq.Init.Logic.True
                                          )
                                        ) H Q
                                      )
                                    )
                                  )
                                )
                              )
                            )
                          )
                        ) H Q
                      ) (
                        (
                          forall x : A_,
                          forall y : B_,
                          forall l :
                            Coq.Init.Datatypes.list (
                              Coq.Init.Datatypes.prod A_ B_
                            ),
                          Coq.Init.Logic.not (
                            Coq.Init.Logic.eq x0__ (
                              Coq.Lists.List.cons (x, y) l : Coq.Init.Datatypes.list (
                                  Coq.Init.Datatypes.prod A_ B_
                                )
                            )
                          )
                        ) ->
                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                          CFML.CFHeaps.local (
                            fun H : CFML.CFHeaps.hprop =>
                            fun Q : _ -> CFML.CFHeaps.hprop =>
                            Coq.Init.Logic.True
                          )
                        ) H Q
                      )
                    )
                  ) H Q
                )
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def split (
          Coq.Lists.List.cons (
            @CFML.CFHeaps.dyn (
              Coq.Init.Datatypes.list (Coq.Init.Datatypes.prod A_ B_)
            ) x0__
          ) Coq.Lists.List.nil
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF split) => CFHeader_Provide split__cf.

Parameter combine : CFML.CFApp.func.

Parameter combine__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat combine) (
        forall B_ : Type,
        forall A_ : Type,
        forall l1 : Coq.Init.Datatypes.list A_,
        forall l2 : Coq.Init.Datatypes.list B_,
        forall H : CFML.CFHeaps.hprop,
        forall Q :
          Coq.Init.Datatypes.list (Coq.Init.Datatypes.prod A_ B_) ->
          CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_val (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            forall x0__ :
              Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
                Coq.Init.Datatypes.list B_
              ),
            Coq.Init.Logic.eq x0__ (l1, l2) ->
            CFML.CFPrint.tag CFML.CFPrint.tag_match (
              CFML.CFHeaps.local (
                CFML.CFPrint.tag CFML.CFPrint.tag_case (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      Coq.Init.Logic.eq x0__ (
                        (Coq.Lists.List.nil : Coq.Init.Datatypes.list A_),
                        (Coq.Lists.List.nil : Coq.Init.Datatypes.list B_)
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (
                            Q (
                              Coq.Lists.List.nil : Coq.Init.Datatypes.list (
                                  Coq.Init.Datatypes.prod A_ B_
                                )
                            )
                          )
                        )
                      ) H Q
                    ) (
                      Coq.Init.Logic.not (
                        Coq.Init.Logic.eq x0__ (
                          (Coq.Lists.List.nil : Coq.Init.Datatypes.list A_),
                          (Coq.Lists.List.nil : Coq.Init.Datatypes.list B_)
                        )
                      ) ->
                      CFML.CFPrint.tag CFML.CFPrint.tag_case (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          Coq.Init.Logic.and (
                            forall a1 : A_,
                            forall l1 : Coq.Init.Datatypes.list A_,
                            forall a2 : B_,
                            forall l2 : Coq.Init.Datatypes.list B_,
                            Coq.Init.Logic.eq x0__ (
                              (
                                Coq.Lists.List.cons a1 l1 : Coq.Init.Datatypes.list A_
                              ),
                              (
                                Coq.Lists.List.cons a2 l2 : Coq.Init.Datatypes.list B_
                              )
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_let (
                              CFML.CFHeaps.local (
                                CFML.CFPrint.cf_let (
                                  CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                    @CFML.CFApp.app_def combine (
                                      Coq.Lists.List.cons (
                                        @CFML.CFHeaps.dyn (
                                          Coq.Init.Datatypes.list A_
                                        ) l1
                                      ) (
                                        Coq.Lists.List.cons (
                                          @CFML.CFHeaps.dyn (
                                            Coq.Init.Datatypes.list B_
                                          ) l2
                                        ) Coq.Lists.List.nil
                                      )
                                    ) (
                                      Coq.Init.Datatypes.list (
                                        Coq.Init.Datatypes.prod A_ B_
                                      )
                                    )
                                  )
                                ) (
                                  fun x1__ :
                                    Coq.Init.Datatypes.list (
                                      Coq.Init.Datatypes.prod A_ B_
                                    )
                                  =>
                                  CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                    CFML.CFHeaps.local (
                                      fun H : CFML.CFHeaps.hprop =>
                                      fun Q : _ -> CFML.CFHeaps.hprop =>
                                      TLC.LibLogic.pred_incl H (
                                        Q (
                                          Coq.Lists.List.cons (a1, a2) x1__ : Coq.Init.Datatypes.list (
                                              Coq.Init.Datatypes.prod A_ B_
                                            )
                                        )
                                      )
                                    )
                                  )
                                )
                              )
                            ) H Q
                          ) (
                            (
                              forall a1 : A_,
                              forall l1 : Coq.Init.Datatypes.list A_,
                              forall a2 : B_,
                              forall l2 : Coq.Init.Datatypes.list B_,
                              Coq.Init.Logic.not (
                                Coq.Init.Logic.eq x0__ (
                                  (
                                    Coq.Lists.List.cons a1 l1 : Coq.Init.Datatypes.list A_
                                  ),
                                  (
                                    Coq.Lists.List.cons a2 l2 : Coq.Init.Datatypes.list B_
                                  )
                                )
                              )
                            ) ->
                            CFML.CFPrint.tag CFML.CFPrint.tag_case (
                              CFML.CFHeaps.local (
                                fun H : CFML.CFHeaps.hprop =>
                                fun Q : _ -> CFML.CFHeaps.hprop =>
                                Coq.Init.Logic.and (
                                  forall p0__ : Coq.Init.Datatypes.list A_,
                                  forall p1__ : Coq.Init.Datatypes.list B_,
                                  Coq.Init.Logic.eq x0__ (p0__, p1__) ->
                                  CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                                    CFML.CFHeaps.local (
                                      fun H : CFML.CFHeaps.hprop =>
                                      fun Q : _ -> CFML.CFHeaps.hprop =>
                                      Coq.Init.Logic.False
                                    )
                                  ) H Q
                                ) (
                                  (
                                    forall p0__ : Coq.Init.Datatypes.list A_,
                                    forall p1__ : Coq.Init.Datatypes.list B_,
                                    Coq.Init.Logic.not (
                                      Coq.Init.Logic.eq x0__ (p0__, p1__)
                                    )
                                  ) ->
                                  CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                    CFML.CFHeaps.local (
                                      fun H : CFML.CFHeaps.hprop =>
                                      fun Q : _ -> CFML.CFHeaps.hprop =>
                                      Coq.Init.Logic.True
                                    )
                                  ) H Q
                                )
                              )
                            ) H Q
                          )
                        )
                      ) H Q
                    )
                  )
                )
              )
            ) H Q
          )
        ) H Q ->
        CFML.CFApp.app_def combine (
          Coq.Lists.List.cons (
            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l1
          ) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l2
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF combine) => CFHeader_Provide combine__cf.

Parameter take : CFML.CFApp.func.

Parameter take__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat take) (
        forall A_ : Type,
        forall n : Coq.ZArith.BinInt.Z,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_seq (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            Coq.Init.Logic.ex (
              fun Q' : _ -> CFML.CFHeaps.hprop =>
              Coq.Init.Logic.and (
                CFML.CFPrint.tag CFML.CFPrint.tag_assert (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (
                            Q (
                              (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) n (
                                0
                              )%Z
                            )
                          )
                        )
                      ) H (
                        fun _b : Coq.Init.Datatypes.bool =>
                        CFML.CFHeaps.heap_is_star (
                          CFML.CFHeaps.heap_is_empty_st (
                            Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
                          )
                        ) H
                      )
                    ) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
                  )
                ) H Q'
              ) (
                CFML.CFPrint.tag CFML.CFPrint.tag_fun (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    forall aux : CFML.CFApp.func,
                    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
                      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                        forall B_ : Type,
                        forall n : Coq.ZArith.BinInt.Z,
                        forall l : Coq.Init.Datatypes.list B_,
                        forall H : CFML.CFHeaps.hprop,
                        forall Q :
                          Coq.Init.Datatypes.list B_ -> CFML.CFHeaps.hprop,
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  TLC.LibLogic.pred_incl H (
                                    Q (
                                      (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
                                        0
                                      )%Z
                                    )
                                  )
                                )
                              )
                            ) (
                              fun x0__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (
                                          Q (
                                            Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                          )
                                        )
                                      )
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_val (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        forall x1__ :
                                          Coq.Init.Datatypes.list B_,
                                        Coq.Init.Logic.eq x1__ l ->
                                        CFML.CFPrint.tag CFML.CFPrint.tag_match (
                                          CFML.CFHeaps.local (
                                            CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                              CFML.CFHeaps.local (
                                                fun H : CFML.CFHeaps.hprop =>
                                                fun Q :
                                                  _ -> CFML.CFHeaps.hprop
                                                =>
                                                Coq.Init.Logic.and (
                                                  Coq.Init.Logic.eq x1__ (
                                                    Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.False
                                                    )
                                                  ) H Q
                                                ) (
                                                  Coq.Init.Logic.not (
                                                    Coq.Init.Logic.eq x1__ (
                                                      Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                    )
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.and (
                                                        forall a : B_,
                                                        forall l :
                                                          Coq.Init.Datatypes.list B_,
                                                        Coq.Init.Logic.eq x1__ (
                                                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                                          CFML.CFHeaps.local (
                                                            CFML.CFPrint.cf_let (
                                                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                                                @CFML.CFApp.app_def aux (
                                                                  Coq.Lists.List.cons (
                                                                    @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                                      Coq.ZArith.BinInt.Z.sub n (
                                                                        1
                                                                      )%Z
                                                                    )
                                                                  ) (
                                                                    Coq.Lists.List.cons (
                                                                      @CFML.CFHeaps.dyn (
                                                                        Coq.Init.Datatypes.list B_
                                                                      ) l
                                                                    ) Coq.Lists.List.nil
                                                                  )
                                                                ) (
                                                                  Coq.Init.Datatypes.list B_
                                                                )
                                                              )
                                                            ) (
                                                              fun x2__ :
                                                                Coq.Init.Datatypes.list B_
                                                              =>
                                                              CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                                                CFML.CFHeaps.local (
                                                                  fun H :
                                                                    CFML.CFHeaps.hprop
                                                                  =>
                                                                  fun Q :
                                                                    _ ->
                                                                    CFML.CFHeaps.hprop
                                                                  =>
                                                                  TLC.LibLogic.pred_incl H (
                                                                    Q (
                                                                      Coq.Lists.List.cons a x2__ : Coq.Init.Datatypes.list B_
                                                                    )
                                                                  )
                                                                )
                                                              )
                                                            )
                                                          )
                                                        ) H Q
                                                      ) (
                                                        (
                                                          forall a : B_,
                                                          forall l :
                                                            Coq.Init.Datatypes.list B_,
                                                          Coq.Init.Logic.not (
                                                            Coq.Init.Logic.eq x1__ (
                                                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                            )
                                                          )
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                                          CFML.CFHeaps.local (
                                                            fun H :
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            fun Q :
                                                              _ ->
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            Coq.Init.Logic.True
                                                          )
                                                        ) H Q
                                                      )
                                                    )
                                                  ) H Q
                                                )
                                              )
                                            )
                                          )
                                        ) H Q
                                      )
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q ->
                        CFML.CFApp.app_def aux (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                          ) (
                            Coq.Lists.List.cons (
                              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l
                            ) Coq.Lists.List.nil
                          )
                        ) H Q
                      )
                    ) ->
                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                      @CFML.CFApp.app_def aux (
                        Coq.Lists.List.cons (
                          @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                        ) (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                          ) Coq.Lists.List.nil
                        )
                      ) (Coq.Init.Datatypes.list A_)
                    ) H Q
                  )
                ) (Q' Coq.Init.Datatypes.tt) Q
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def take (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF take) => CFHeader_Provide take__cf.

Parameter drop : CFML.CFApp.func.

Parameter drop__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat drop) (
        forall A_ : Type,
        forall n : Coq.ZArith.BinInt.Z,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q : Coq.Init.Datatypes.list A_ -> CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_seq (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            Coq.Init.Logic.ex (
              fun Q' : _ -> CFML.CFHeaps.hprop =>
              Coq.Init.Logic.and (
                CFML.CFPrint.tag CFML.CFPrint.tag_assert (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (
                            Q (
                              (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) n (
                                0
                              )%Z
                            )
                          )
                        )
                      ) H (
                        fun _b : Coq.Init.Datatypes.bool =>
                        CFML.CFHeaps.heap_is_star (
                          CFML.CFHeaps.heap_is_empty_st (
                            Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
                          )
                        ) H
                      )
                    ) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
                  )
                ) H Q'
              ) (
                CFML.CFPrint.tag CFML.CFPrint.tag_fun (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    forall aux : CFML.CFApp.func,
                    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
                      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                        forall B_ : Type,
                        forall n : Coq.ZArith.BinInt.Z,
                        forall l : Coq.Init.Datatypes.list B_,
                        forall H : CFML.CFHeaps.hprop,
                        forall Q :
                          Coq.Init.Datatypes.list B_ -> CFML.CFHeaps.hprop,
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  TLC.LibLogic.pred_incl H (
                                    Q (
                                      (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
                                        0
                                      )%Z
                                    )
                                  )
                                )
                              )
                            ) (
                              fun x0__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (Q l)
                                      )
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_val (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        forall x1__ :
                                          Coq.Init.Datatypes.list B_,
                                        Coq.Init.Logic.eq x1__ l ->
                                        CFML.CFPrint.tag CFML.CFPrint.tag_match (
                                          CFML.CFHeaps.local (
                                            CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                              CFML.CFHeaps.local (
                                                fun H : CFML.CFHeaps.hprop =>
                                                fun Q :
                                                  _ -> CFML.CFHeaps.hprop
                                                =>
                                                Coq.Init.Logic.and (
                                                  Coq.Init.Logic.eq x1__ (
                                                    Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.False
                                                    )
                                                  ) H Q
                                                ) (
                                                  Coq.Init.Logic.not (
                                                    Coq.Init.Logic.eq x1__ (
                                                      Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                    )
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.and (
                                                        forall a : B_,
                                                        forall l :
                                                          Coq.Init.Datatypes.list B_,
                                                        Coq.Init.Logic.eq x1__ (
                                                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                                          @CFML.CFApp.app_def aux (
                                                            Coq.Lists.List.cons (
                                                              @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                                Coq.ZArith.BinInt.Z.sub n (
                                                                  1
                                                                )%Z
                                                              )
                                                            ) (
                                                              Coq.Lists.List.cons (
                                                                @CFML.CFHeaps.dyn (
                                                                  Coq.Init.Datatypes.list B_
                                                                ) l
                                                              ) Coq.Lists.List.nil
                                                            )
                                                          ) (
                                                            Coq.Init.Datatypes.list B_
                                                          )
                                                        ) H Q
                                                      ) (
                                                        (
                                                          forall a : B_,
                                                          forall l :
                                                            Coq.Init.Datatypes.list B_,
                                                          Coq.Init.Logic.not (
                                                            Coq.Init.Logic.eq x1__ (
                                                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                            )
                                                          )
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                                          CFML.CFHeaps.local (
                                                            fun H :
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            fun Q :
                                                              _ ->
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            Coq.Init.Logic.True
                                                          )
                                                        ) H Q
                                                      )
                                                    )
                                                  ) H Q
                                                )
                                              )
                                            )
                                          )
                                        ) H Q
                                      )
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q ->
                        CFML.CFApp.app_def aux (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                          ) (
                            Coq.Lists.List.cons (
                              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l
                            ) Coq.Lists.List.nil
                          )
                        ) H Q
                      )
                    ) ->
                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                      @CFML.CFApp.app_def aux (
                        Coq.Lists.List.cons (
                          @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                        ) (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                          ) Coq.Lists.List.nil
                        )
                      ) (Coq.Init.Datatypes.list A_)
                    ) H Q
                  )
                ) (Q' Coq.Init.Datatypes.tt) Q
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def drop (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF drop) => CFHeader_Provide drop__cf.

Parameter split_at : CFML.CFApp.func.

Parameter split_at__cf :
  CFML.CFPrint.tag CFML.CFPrint.tag_top_fun (
    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat split_at) (
        forall A_ : Type,
        forall n : Coq.ZArith.BinInt.Z,
        forall l : Coq.Init.Datatypes.list A_,
        forall H : CFML.CFHeaps.hprop,
        forall Q :
          Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
            Coq.Init.Datatypes.list A_
          ) ->
          CFML.CFHeaps.hprop,
        CFML.CFPrint.tag CFML.CFPrint.tag_seq (
          CFML.CFHeaps.local (
            fun H : CFML.CFHeaps.hprop =>
            fun Q : _ -> CFML.CFHeaps.hprop =>
            Coq.Init.Logic.ex (
              fun Q' : _ -> CFML.CFHeaps.hprop =>
              Coq.Init.Logic.and (
                CFML.CFPrint.tag CFML.CFPrint.tag_assert (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    Coq.Init.Logic.and (
                      CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                        CFML.CFHeaps.local (
                          fun H : CFML.CFHeaps.hprop =>
                          fun Q : _ -> CFML.CFHeaps.hprop =>
                          TLC.LibLogic.pred_incl H (
                            Q (
                              (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (@TLC.LibOrder.ge _ (@TLC.LibOrder.ge_of_le _ TLC.LibInt.le_int_inst) x__ y__)) n (
                                0
                              )%Z
                            )
                          )
                        )
                      ) H (
                        fun _b : Coq.Init.Datatypes.bool =>
                        CFML.CFHeaps.heap_is_star (
                          CFML.CFHeaps.heap_is_empty_st (
                            Coq.Init.Logic.eq _b Coq.Init.Datatypes.true
                          )
                        ) H
                      )
                    ) (TLC.LibLogic.pred_incl H (Q Coq.Init.Datatypes.tt))
                  )
                ) H Q'
              ) (
                CFML.CFPrint.tag CFML.CFPrint.tag_fun (
                  CFML.CFHeaps.local (
                    fun H : CFML.CFHeaps.hprop =>
                    fun Q : _ -> CFML.CFHeaps.hprop =>
                    forall aux : CFML.CFApp.func,
                    CFML.CFPrint.tag CFML.CFPrint.tag_app_curried (
                      Coq.Init.Logic.and (CFML.CFApp.curried (2)%nat aux) (
                        forall B_ : Type,
                        forall n : Coq.ZArith.BinInt.Z,
                        forall l : Coq.Init.Datatypes.list B_,
                        forall H : CFML.CFHeaps.hprop,
                        forall Q :
                          Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list B_) (
                            Coq.Init.Datatypes.list B_
                          ) ->
                          CFML.CFHeaps.hprop,
                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                          CFML.CFHeaps.local (
                            CFML.CFPrint.cf_let (
                              CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  TLC.LibLogic.pred_incl H (
                                    Q (
                                      (fun x__ y__ : Coq.ZArith.BinInt.Z => TLC.LibReflect.isTrue (Coq.Init.Logic.eq x__ y__)) n (
                                        0
                                      )%Z
                                    )
                                  )
                                )
                              )
                            ) (
                              fun x0__ : Coq.Init.Datatypes.bool =>
                              CFML.CFPrint.tag CFML.CFPrint.tag_if (
                                CFML.CFHeaps.local (
                                  fun H : CFML.CFHeaps.hprop =>
                                  fun Q : _ -> CFML.CFHeaps.hprop =>
                                  Coq.Init.Logic.and (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.true ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        TLC.LibLogic.pred_incl H (
                                          Q (
                                            (
                                              Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                            ),
                                            l
                                          )
                                        )
                                      )
                                    ) H Q
                                  ) (
                                    Coq.Init.Logic.eq x0__ Coq.Init.Datatypes.false ->
                                    CFML.CFPrint.tag CFML.CFPrint.tag_val (
                                      CFML.CFHeaps.local (
                                        fun H : CFML.CFHeaps.hprop =>
                                        fun Q : _ -> CFML.CFHeaps.hprop =>
                                        forall x1__ :
                                          Coq.Init.Datatypes.list B_,
                                        Coq.Init.Logic.eq x1__ l ->
                                        CFML.CFPrint.tag CFML.CFPrint.tag_match (
                                          CFML.CFHeaps.local (
                                            CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                              CFML.CFHeaps.local (
                                                fun H : CFML.CFHeaps.hprop =>
                                                fun Q :
                                                  _ -> CFML.CFHeaps.hprop
                                                =>
                                                Coq.Init.Logic.and (
                                                  Coq.Init.Logic.eq x1__ (
                                                    Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_fail (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.False
                                                    )
                                                  ) H Q
                                                ) (
                                                  Coq.Init.Logic.not (
                                                    Coq.Init.Logic.eq x1__ (
                                                      Coq.Lists.List.nil : Coq.Init.Datatypes.list B_
                                                    )
                                                  ) ->
                                                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                                    CFML.CFHeaps.local (
                                                      fun H :
                                                        CFML.CFHeaps.hprop
                                                      =>
                                                      fun Q :
                                                        _ -> CFML.CFHeaps.hprop
                                                      =>
                                                      Coq.Init.Logic.and (
                                                        forall a : B_,
                                                        forall l :
                                                          Coq.Init.Datatypes.list B_,
                                                        Coq.Init.Logic.eq x1__ (
                                                          Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_let (
                                                          CFML.CFHeaps.local (
                                                            CFML.CFPrint.cf_let (
                                                              CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                                                                @CFML.CFApp.app_def aux (
                                                                  Coq.Lists.List.cons (
                                                                    @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z (
                                                                      Coq.ZArith.BinInt.Z.sub n (
                                                                        1
                                                                      )%Z
                                                                    )
                                                                  ) (
                                                                    Coq.Lists.List.cons (
                                                                      @CFML.CFHeaps.dyn (
                                                                        Coq.Init.Datatypes.list B_
                                                                      ) l
                                                                    ) Coq.Lists.List.nil
                                                                  )
                                                                ) (
                                                                  Coq.Init.Datatypes.prod (
                                                                    Coq.Init.Datatypes.list B_
                                                                  ) (
                                                                    Coq.Init.Datatypes.list B_
                                                                  )
                                                                )
                                                              )
                                                            ) (
                                                              fun x2__ :
                                                                Coq.Init.Datatypes.prod (
                                                                  Coq.Init.Datatypes.list B_
                                                                ) (
                                                                  Coq.Init.Datatypes.list B_
                                                                )
                                                              =>
                                                              CFML.CFPrint.tag CFML.CFPrint.tag_match (
                                                                CFML.CFHeaps.local (
                                                                  CFML.CFPrint.tag CFML.CFPrint.tag_case (
                                                                    CFML.CFHeaps.local (
                                                                      fun H :
                                                                        CFML.CFHeaps.hprop
                                                                      =>
                                                                      fun Q :
                                                                        _ ->
                                                                        CFML.CFHeaps.hprop
                                                                      =>
                                                                      Coq.Init.Logic.and (
                                                                        forall l1 :
                                                                          Coq.Init.Datatypes.list B_,
                                                                        forall l2 :
                                                                          Coq.Init.Datatypes.list B_,
                                                                        Coq.Init.Logic.eq x2__ (
                                                                          l1,
                                                                          l2
                                                                        ) ->
                                                                        CFML.CFPrint.tag CFML.CFPrint.tag_ret (
                                                                          CFML.CFHeaps.local (
                                                                            fun H :
                                                                              CFML.CFHeaps.hprop
                                                                            =>
                                                                            fun Q :
                                                                              _ ->
                                                                              CFML.CFHeaps.hprop
                                                                            =>
                                                                            TLC.LibLogic.pred_incl H (
                                                                              Q (
                                                                                (
                                                                                  Coq.Lists.List.cons a l1 : Coq.Init.Datatypes.list B_
                                                                                ),
                                                                                l2
                                                                              )
                                                                            )
                                                                          )
                                                                        ) H Q
                                                                      ) (
                                                                        (
                                                                          forall l1 :
                                                                            Coq.Init.Datatypes.list B_,
                                                                          forall l2 :
                                                                            Coq.Init.Datatypes.list B_,
                                                                          Coq.Init.Logic.not (
                                                                            Coq.Init.Logic.eq x2__ (
                                                                              l1,
                                                                              l2
                                                                            )
                                                                          )
                                                                        ) ->
                                                                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                                                          CFML.CFHeaps.local (
                                                                            fun H :
                                                                              CFML.CFHeaps.hprop
                                                                            =>
                                                                            fun Q :
                                                                              _ ->
                                                                              CFML.CFHeaps.hprop
                                                                            =>
                                                                            Coq.Init.Logic.True
                                                                          )
                                                                        ) H Q
                                                                      )
                                                                    )
                                                                  )
                                                                )
                                                              )
                                                            )
                                                          )
                                                        ) H Q
                                                      ) (
                                                        (
                                                          forall a : B_,
                                                          forall l :
                                                            Coq.Init.Datatypes.list B_,
                                                          Coq.Init.Logic.not (
                                                            Coq.Init.Logic.eq x1__ (
                                                              Coq.Lists.List.cons a l : Coq.Init.Datatypes.list B_
                                                            )
                                                          )
                                                        ) ->
                                                        CFML.CFPrint.tag CFML.CFPrint.tag_done (
                                                          CFML.CFHeaps.local (
                                                            fun H :
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            fun Q :
                                                              _ ->
                                                              CFML.CFHeaps.hprop
                                                            =>
                                                            Coq.Init.Logic.True
                                                          )
                                                        ) H Q
                                                      )
                                                    )
                                                  ) H Q
                                                )
                                              )
                                            )
                                          )
                                        ) H Q
                                      )
                                    ) H Q
                                  )
                                )
                              )
                            )
                          )
                        ) H Q ->
                        CFML.CFApp.app_def aux (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                          ) (
                            Coq.Lists.List.cons (
                              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list B_) l
                            ) Coq.Lists.List.nil
                          )
                        ) H Q
                      )
                    ) ->
                    CFML.CFPrint.tag CFML.CFPrint.tag_apply (
                      @CFML.CFApp.app_def aux (
                        Coq.Lists.List.cons (
                          @CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n
                        ) (
                          Coq.Lists.List.cons (
                            @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
                          ) Coq.Lists.List.nil
                        )
                      ) (
                        Coq.Init.Datatypes.prod (Coq.Init.Datatypes.list A_) (
                          Coq.Init.Datatypes.list A_
                        )
                      )
                    ) H Q
                  )
                ) (Q' Coq.Init.Datatypes.tt) Q
              )
            )
          )
        ) H Q ->
        CFML.CFApp.app_def split_at (
          Coq.Lists.List.cons (@CFML.CFHeaps.dyn Coq.ZArith.BinInt.Z n) (
            Coq.Lists.List.cons (
              @CFML.CFHeaps.dyn (Coq.Init.Datatypes.list A_) l
            ) Coq.Lists.List.nil
          )
        ) H Q
      )
    )
  ).

Hint Extern 1 (RegisterCF split_at) => CFHeader_Provide split_at__cf.