{-# LANGUAGE BangPatterns #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE EmptyDataDecls #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE NoMonomorphismRestriction #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}

{-# OPTIONS_GHC -Wno-overlapping-patterns #-}

module MAlonzo.Code.Data.List.Extrema where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Extrema.Core
import qualified MAlonzo.Code.Data.List.Membership.Propositional
import qualified MAlonzo.Code.Data.List.Membership.Propositional.Properties
import qualified MAlonzo.Code.Data.List.Membership.Setoid.Properties
import qualified MAlonzo.Code.Data.List.Properties
import qualified MAlonzo.Code.Data.List.Relation.Unary.All
import qualified MAlonzo.Code.Data.List.Relation.Unary.Any
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.List.Extrema._._<_
d__'60'__102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny -> ()
d__'60'__102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'60'__102 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.List.Extrema.argmin
d_argmin_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmin_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmin_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_argmin_140 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.argmax
d_argmax_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_argmax_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_argmax_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_argmax_144 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
-- Data.List.Extrema.min
d_min_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min_148 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min_148 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_148 T_TotalOrder_986
v3
du_min_148 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min_148 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min_148 T_TotalOrder_986
v0 = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max
d_max_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_max_150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_max_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_150 T_TotalOrder_986
v3
du_max_150 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_max_150 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_max_150 T_TotalOrder_986
v0 = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema._.f[argmin]≤v⁺
d_f'91'argmin'93''8804'v'8314'_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_f'91'argmin'93''8804'v'8314'_168 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_f'91'argmin'93''8804'v'8314'_168 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''8804'v'8314'_168 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4432
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''8804'v_216
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmin]<v⁺
d_f'91'argmin'93''60'v'8314'_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmin'93''60'v'8314'_178 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_f'91'argmin'93''60'v'8314'_178 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_f'91'argmin'93''60'v'8314'_178 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4432
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7506''45''60'v_228
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v≤f[argmin]⁺
d_v'8804'f'91'argmin'93''8314'_188 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'f'91'argmin'93''8314'_188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'f'91'argmin'93''8314'_188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'8804'f'91'argmin'93''8314'_188 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4392
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'8804'_240
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.v<f[argmin]⁺
d_v'60'f'91'argmin'93''8314'_198 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmin'93''8314'_198 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'f'91'argmin'93''8314'_198 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_198 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_v'60'f'91'argmin'93''8314'_198 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmin'93''8314'_198 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4392
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'pres'7495''45'v'60'_256
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmin]≤f[⊤]
d_f'91'argmin'93''8804'f'91''8868''93'_204 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_204 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91'argmin'93''8804'f'91''8868''93'_204 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_204 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91''8868''93'_204 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_204 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_204 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
            ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
               ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                  ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                     (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))
-- Data.List.Extrema._.f[argmin]≤f[xs]
d_f'91'argmin'93''8804'f'91'xs'93'_216 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_216 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'argmin'93''8804'f'91'xs'93'_216 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_216 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'argmin'93''8804'f'91'xs'93'_216 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_216 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_216 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_4370
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'forces'7495''45'v'8804'_272
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
-- Data.List.Extrema._.f[argmin]≈f[v]⁺
d_f'91'argmin'93''8776'f'91'v'93''8314'_230 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_230 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmin'93''8776'f'91'v'93''8314'_230 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_230
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmin'93''8776'f'91'v'93''8314'_230 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_230 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_230 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
      (T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
         ((T_TotalOrder_986 -> T_IsTotalOrder_488)
-> AgdaAny -> T_IsTotalOrder_488
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmin_140 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
                  ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                     ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                        ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                           (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
-- Data.List.Extrema.argmin[xs]≤argmin[ys]⁺
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin[xs]<argmin[ys]⁺
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 AgdaAny
v4 [AgdaAny]
v6
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v4) AgdaAny
v3 [AgdaAny]
v5 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v2 AgdaAny
v9) AgdaAny
v3 [AgdaAny]
v5))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v6) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmin-sel
d_argmin'45'sel_300 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmin'45'sel_300 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmin'45'sel_300 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_300 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_argmin'45'sel_300 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmin'45'sel_300 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmin'45'sel_300 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_732
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_204
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmin-all
d_argmin'45'all_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmin'45'all_312 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmin'45'all_312 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 ~AgdaAny -> T_Level_18
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_312 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 AgdaAny
v11 T_All_44
v12
du_argmin'45'all_312 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmin'45'all_312 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmin'45'all_312 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: AgdaAny
v6
          = (T_Setoid_46
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_46
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1970
              (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
              ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480'_198 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8851''7480''45'sel_204
                 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_436 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema._.v≤f[argmax]⁺
d_v'8804'f'91'argmax'93''8314'_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'f'91'argmax'93''8314'_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'f'91'argmax'93''8314'_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'8804'f'91'argmax'93''8314'_374 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4432
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'8804'_300
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.v<f[argmax]⁺
d_v'60'f'91'argmax'93''8314'_384 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'f'91'argmax'93''8314'_384 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'f'91'argmax'93''8314'_384 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7
du_v'60'f'91'argmax'93''8314'_384 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30 -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7506'_4432
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7506''45'v'60'_322
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2))
-- Data.List.Extrema._.f[argmax]≤v⁺
d_f'91'argmax'93''8804'v'8314'_394 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_f'91'argmax'93''8804'v'8314'_394 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_f'91'argmax'93''8804'v'8314'_394 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                   [AgdaAny]
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''8804'v'8314'_394 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4392
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''8804'v_344
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[argmax]<v⁺
d_f'91'argmax'93''60'v'8314'_404 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_f'91'argmax'93''60'v'8314'_404 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_f'91'argmax'93''60'v'8314'_404 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny
v7 AgdaAny
v8
                                 [AgdaAny]
v9
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_404 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v8 [AgdaAny]
v9
du_f'91'argmax'93''60'v'8314'_404 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_f'91'argmax'93''60'v'8314'_404 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_404 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
MAlonzo.Code.Data.List.Properties.du_foldr'45'preserves'7495'_4392
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'pres'7495''45''60'v_360
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema._.f[⊥]≤f[argmax]
d_f'91''8869''93''8804'f'91'argmax'93'_410 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_410 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_f'91''8869''93''8804'f'91'argmax'93'_410 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                           AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_410 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91''8869''93''8804'f'91'argmax'93'_410 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_410 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_410 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v2 [AgdaAny]
v3
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
         ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
            ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
               ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                  ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                     (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
            ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))
-- Data.List.Extrema._.f[xs]≤f[argmax]
d_f'91'xs'93''8804'f'91'argmax'93'_422 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_422 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_f'91'xs'93''8804'f'91'argmax'93'_422 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny
v7
                                       [AgdaAny]
v8
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_422 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 [AgdaAny]
v8
du_f'91'xs'93''8804'f'91'argmax'93'_422 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_422 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_422 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_All_44
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
MAlonzo.Code.Data.List.Properties.du_foldr'45'forces'7495'_4370
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'forces'7495''45''8804'v_376
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3)))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
      ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
         ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
            ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
               ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                  (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
         ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> AgdaAny
v1
            (((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
               ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3))))
-- Data.List.Extrema._.f[argmax]≈f[v]⁺
d_f'91'argmax'93''8776'f'91'v'93''8314'_436 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_436 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_f'91'argmax'93''8776'f'91'v'93''8314'_436 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5
                                            AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_436
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 [AgdaAny]
v9 T_Any_34
v10 T_All_44
v11 AgdaAny
v12
du_f'91'argmax'93''8776'f'91'v'93''8314'_436 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_436 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_436 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 [AgdaAny]
v4 T_Any_34
v5 T_All_44
v6
                                             AgdaAny
v7
  = (T_IsPartialOrder_248
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_antisym_258
      (T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
         ((T_TotalOrder_986 -> T_IsTotalOrder_488)
-> AgdaAny -> T_IsTotalOrder_488
forall a b. a -> b
coe
            T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)))
      ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_argmax_144 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4)) ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v4 AgdaAny
v7 T_All_44
v6)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2) AgdaAny
v3 [AgdaAny]
v4
         ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
            ((AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 AgdaAny
v2 [AgdaAny]
v4 T_Any_34
v5
               ((T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
                  ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
                     ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
                        ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
                           (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
                  ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v2)))))
-- Data.List.Extrema.argmax[xs]≤argmax[ys]⁺
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
                                                   ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                                                    [AgdaAny]
v5 [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax[xs]<argmax[ys]⁺
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4
                                                 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490
      T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 [AgdaAny]
v10 [AgdaAny]
v11 T__'8846'__30
v12 T_All_44
v13
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 [AgdaAny]
v5
                                                  [AgdaAny]
v6 T__'8846'__30
v7 T_All_44
v8
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_404 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v3 [AgdaAny]
v5
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v3) AgdaAny
v4 [AgdaAny]
v6 T__'8846'__30
v7)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_All_44 -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v9 ->
               (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v2 ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1 AgdaAny
v9) AgdaAny
v4 [AgdaAny]
v6))
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) (T_All_44 -> AgdaAny
forall a b. a -> b
coe T_All_44
v8))
-- Data.List.Extrema.argmax-sel
d_argmax'45'sel_506 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_argmax'45'sel_506 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
d_argmax'45'sel_506 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 AgdaAny -> AgdaAny
v6
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_506 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v6
du_argmax'45'sel_506 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_argmax'45'sel_506 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T__'8846'__30
du_argmax'45'sel_506 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Propositional.Properties.du_foldr'45'selective_732
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
      ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_288
         (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
-- Data.List.Extrema.argmax-all
d_argmax'45'all_518 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_argmax'45'all_518 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_argmax'45'all_518 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 AgdaAny -> AgdaAny
v7 ~AgdaAny -> T_Level_18
v8 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11
                    T_All_44
v12
  = T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_518 T_TotalOrder_986
v3 AgdaAny -> AgdaAny
v7 AgdaAny
v9 [AgdaAny]
v10 AgdaAny
v11 T_All_44
v12
du_argmax'45'all_518 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_argmax'45'all_518 :: T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_argmax'45'all_518 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 AgdaAny
v4 T_All_44
v5
  = let v6 :: AgdaAny
v6
          = (T_Setoid_46
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              T_Setoid_46
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
MAlonzo.Code.Data.List.Membership.Setoid.Properties.du_foldr'45'selective_1970
              (T_Setoid_46 -> AgdaAny
forall a b. a -> b
coe
                 T_Setoid_46
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
              ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_TotalOrder_986 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480'_200 T_TotalOrder_986
v0 AgdaAny -> AgdaAny
v1)
              ((T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.List.Extrema.Core.du_'8852''7480''45'sel_288
                 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v1))
              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v6 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
           -> ([AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny)
-> [AgdaAny] -> T_All_44 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                [AgdaAny] -> T_All_44 -> T_Any_34 -> AgdaAny
MAlonzo.Code.Data.List.Relation.Unary.All.du_lookup_436 [AgdaAny]
v3 T_All_44
v5 AgdaAny
v7
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.List.Extrema.min≤v⁺
d_min'8804'v'8314'_572 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_min'8804'v'8314'_572 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_min'8804'v'8314'_572 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_572 T_TotalOrder_986
v3 AgdaAny
v4
du_min'8804'v'8314'_572 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_572 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_min'8804'v'8314'_572 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_f'91'argmin'93''8804'v'8314'_168 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.min<v⁺
d_min'60'v'8314'_582 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'60'v'8314'_582 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_min'60'v'8314'_582 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_582 T_TotalOrder_986
v3 AgdaAny
v4
du_min'60'v'8314'_582 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'60'v'8314'_582 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_min'60'v'8314'_582 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_f'91'argmin'93''60'v'8314'_178 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v≤min⁺
d_v'8804'min'8314'_592 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_v'8804'min'8314'_592 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_v'8804'min'8314'_592 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_592 T_TotalOrder_986
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'8804'min'8314'_592 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_v'8804'min'8314'_592 :: T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_v'8804'min'8314'_592 T_TotalOrder_986
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_v'8804'f'91'argmin'93''8314'_188 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v<min⁺
d_v'60'min'8314'_602 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'min'8314'_602 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_v'60'min'8314'_602 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_602 T_TotalOrder_986
v3 AgdaAny
v5 [AgdaAny]
v6
du_v'60'min'8314'_602 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'min'8314'_602 :: T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_v'60'min'8314'_602 T_TotalOrder_986
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_v'60'f'91'argmin'93''8314'_198 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.min≤⊤
d_min'8804''8868'_608 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_min'8804''8868'_608 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_min'8804''8868'_608 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_608 T_TotalOrder_986
v3
du_min'8804''8868'_608 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_608 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_min'8804''8868'_608 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91'argmin'93''8804'f'91''8868''93'_204 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≤xs
d_min'8804'xs_616 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_min'8804'xs_616 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_min'8804'xs_616 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_616 T_TotalOrder_986
v3
du_min'8804'xs_616 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_min'8804'xs_616 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
du_min'8804'xs_616 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'argmin'93''8804'f'91'xs'93'_216 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min≈v⁺
d_min'8776'v'8314'_626 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_min'8776'v'8314'_626 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_min'8776'v'8314'_626 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_626 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_min'8776'v'8314'_626 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_min'8776'v'8314'_626 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_min'8776'v'8314'_626 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmin'93''8776'f'91'v'93''8314'_230 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.min[xs]≤min[ys]⁺
d_min'91'xs'93''8804'min'91'ys'93''8314'_642 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_642 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_min'91'xs'93''8804'min'91'ys'93''8314'_642 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 T_TotalOrder_986
v3
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmin'91'xs'93''8804'argmin'91'ys'93''8314'_256 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min[xs]<min[ys]⁺
d_min'91'xs'93''60'min'91'ys'93''8314'_658 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_658 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_min'91'xs'93''60'min'91'ys'93''8314'_658 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_658 T_TotalOrder_986
v3
du_min'91'xs'93''60'min'91'ys'93''8314'_658 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_658 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_min'91'xs'93''60'min'91'ys'93''8314'_658 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmin'91'xs'93''60'argmin'91'ys'93''8314'_284 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.min-mono-⊆
d_min'45'mono'45''8838'_668 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_min'45'mono'45''8838'_668 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_min'45'mono'45''8838'_668 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_668 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_min'45'mono'45''8838'_668 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_min'45'mono'45''8838'_668 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_min'45'mono'45''8838'_668 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_min'91'xs'93''8804'min'91'ys'93''8314'_642 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_266 [AgdaAny]
v4
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_986 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_674 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda0
d_'46'extendedlambda0_674 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_674 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_674 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_674 T_TotalOrder_986
v3 AgdaAny
v10
du_'46'extendedlambda0_674 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda0_674 :: T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda0_674 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
      ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max≤v⁺
d_max'8804'v'8314'_684 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'8804'v'8314'_684 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
d_max'8804'v'8314'_684 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_684 T_TotalOrder_986
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'8804'v'8314'_684 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'8804'v'8314'_684 :: T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> AgdaAny -> T_All_44 -> AgdaAny
du_max'8804'v'8314'_684 T_TotalOrder_986
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> AgdaAny
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
-> T_All_44
-> AgdaAny
du_f'91'argmax'93''8804'v'8314'_394 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.max<v⁺
d_max'60'v'8314'_694 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'60'v'8314'_694 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
d_max'60'v'8314'_694 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_694 T_TotalOrder_986
v3 AgdaAny
v5 [AgdaAny]
v6
du_max'60'v'8314'_694 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'60'v'8314'_694 :: T_TotalOrder_986
-> AgdaAny -> [AgdaAny] -> T_Σ_14 -> T_All_44 -> T_Σ_14
du_max'60'v'8314'_694 T_TotalOrder_986
v0 AgdaAny
v1 [AgdaAny]
v2
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> [AgdaAny]
 -> T_Σ_14
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> [AgdaAny]
-> T_Σ_14
-> T_All_44
-> T_Σ_14
du_f'91'argmax'93''60'v'8314'_404 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v3 -> AgdaAny
v3))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v2)
-- Data.List.Extrema.v≤max⁺
d_v'8804'max'8314'_704 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
d_v'8804'max'8314'_704 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
d_v'8804'max'8314'_704 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_704 T_TotalOrder_986
v3 AgdaAny
v4
du_v'8804'max'8314'_704 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_704 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> AgdaAny
du_v'8804'max'8314'_704 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> AgdaAny
du_v'8804'f'91'argmax'93''8314'_374 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.v<max⁺
d_v'60'max'8314'_714 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_v'60'max'8314'_714 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
d_v'60'max'8314'_714 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_714 T_TotalOrder_986
v3 AgdaAny
v4
du_v'60'max'8314'_714 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_v'60'max'8314'_714 :: T_TotalOrder_986
-> AgdaAny -> AgdaAny -> [AgdaAny] -> T__'8846'__30 -> T_Σ_14
du_v'60'max'8314'_714 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T__'8846'__30
-> T_Σ_14
du_v'60'f'91'argmax'93''8314'_384 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.⊥≤max
d_'8869''8804'max_720 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
d_'8869''8804'max_720 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> AgdaAny
d_'8869''8804'max_720 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_720 T_TotalOrder_986
v3
du_'8869''8804'max_720 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_720 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> AgdaAny
du_'8869''8804'max_720 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
du_f'91''8869''93''8804'f'91'argmax'93'_410 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.xs≤max
d_xs'8804'max_728 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
d_xs'8804'max_728 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> [AgdaAny]
-> T_All_44
d_xs'8804'max_728 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 = T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_728 T_TotalOrder_986
v3
du_xs'8804'max_728 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  [AgdaAny] -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
du_xs'8804'max_728 :: T_TotalOrder_986 -> AgdaAny -> [AgdaAny] -> T_All_44
du_xs'8804'max_728 T_TotalOrder_986
v0
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44)
-> AgdaAny -> AgdaAny -> AgdaAny -> [AgdaAny] -> T_All_44
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> T_All_44
du_f'91'xs'93''8804'f'91'argmax'93'_422 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 -> AgdaAny
v1))
-- Data.List.Extrema.max≈v⁺
d_max'8776'v'8314'_738 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
d_max'8776'v'8314'_738 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
d_max'8776'v'8314'_738 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_738 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6
du_max'8776'v'8314'_738 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  AgdaAny -> AgdaAny
du_max'8776'v'8314'_738 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_max'8776'v'8314'_738 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> T_Any_34
 -> T_All_44
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> T_All_44
-> AgdaAny
-> AgdaAny
du_f'91'argmax'93''8776'f'91'v'93''8314'_436 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v4)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3)
-- Data.List.Extrema.max[xs]≤max[ys]⁺
d_max'91'xs'93''8804'max'91'ys'93''8314'_754 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_754 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
d_max'91'xs'93''8804'max'91'ys'93''8314'_754 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 T_TotalOrder_986
v3 AgdaAny
v4
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_argmax'91'xs'93''8804'argmax'91'ys'93''8314'_462 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max[xs]<max[ys]⁺
d_max'91'xs'93''60'max'91'ys'93''8314'_770 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_770 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
d_max'91'xs'93''60'max'91'ys'93''8314'_770 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_770 T_TotalOrder_986
v3 AgdaAny
v4
du_max'91'xs'93''60'max'91'ys'93''8314'_770 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_770 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_max'91'xs'93''60'max'91'ys'93''8314'_770 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_TotalOrder_986
 -> (AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
forall a b. a -> b
coe
      T_TotalOrder_986
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> T_Σ_14
du_argmax'91'xs'93''60'argmax'91'ys'93''8314'_490 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
-- Data.List.Extrema.max-mono-⊆
d_max'45'mono'45''8838'_780 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
d_max'45'mono'45''8838'_780 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
d_max'45'mono'45''8838'_780 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
  = T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_780 T_TotalOrder_986
v3 AgdaAny
v4 AgdaAny
v5 [AgdaAny]
v6 [AgdaAny]
v7 AgdaAny
v8 AgdaAny -> T_Any_34 -> T_Any_34
v9
du_max'45'mono'45''8838'_780 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny
du_max'45'mono'45''8838'_780 :: T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
du_max'45'mono'45''8838'_780 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4 AgdaAny
v5 AgdaAny -> T_Any_34 -> T_Any_34
v6
  = (T_TotalOrder_986
 -> AgdaAny
 -> AgdaAny
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30
 -> T_All_44
 -> AgdaAny)
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
      T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
-> T_All_44
-> AgdaAny
du_max'91'xs'93''8804'max'91'ys'93''8314'_754 T_TotalOrder_986
v0 AgdaAny
v1 AgdaAny
v2 [AgdaAny]
v3 [AgdaAny]
v4
      ((AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
      (([AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44)
-> [AgdaAny] -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> (AgdaAny -> T_Any_34 -> AgdaAny) -> T_All_44
MAlonzo.Code.Data.List.Relation.Unary.All.du_tabulate_266 [AgdaAny]
v3
         (\ AgdaAny
v7 AgdaAny
v8 ->
            (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
              AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
              (((AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny] -> T_Any_34 -> T_Any_34)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny] -> T_Any_34 -> T_Any_34
MAlonzo.Code.Data.List.Relation.Unary.Any.du_map_76
                 (\ AgdaAny
v9 AgdaAny
v10 -> (T_TotalOrder_986 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_786 (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))
                 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v4) ((AgdaAny -> T_Any_34 -> T_Any_34) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_34 -> T_Any_34
v6 AgdaAny
v7 AgdaAny
v8))))
-- Data.List.Extrema..extendedlambda1
d_'46'extendedlambda1_786 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny ->
  AgdaAny ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  (AgdaAny ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
   MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34) ->
  AgdaAny ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_786 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_TotalOrder_986
-> AgdaAny
-> AgdaAny
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> (AgdaAny -> T_Any_34 -> T_Any_34)
-> AgdaAny
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_786 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_TotalOrder_986
v3 ~AgdaAny
v4 ~AgdaAny
v5 ~[AgdaAny]
v6 ~[AgdaAny]
v7 ~AgdaAny
v8 ~AgdaAny -> T_Any_34 -> T_Any_34
v9
                          AgdaAny
v10 ~T_Any_34
v11 ~AgdaAny
v12 ~T__'8801'__12
v13
  = T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_786 T_TotalOrder_986
v3 AgdaAny
v10
du_'46'extendedlambda1_786 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_TotalOrder_986 ->
  AgdaAny -> AgdaAny
du_'46'extendedlambda1_786 :: T_TotalOrder_986 -> AgdaAny -> AgdaAny
du_'46'extendedlambda1_786 T_TotalOrder_986
v0 AgdaAny
v1
  = (T_IsPreorder_76 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_IsPreorder_76 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_refl_104
      ((T_IsPartialOrder_248 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsPartialOrder_248 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_256
         ((T_IsTotalOrder_488 -> T_IsPartialOrder_248) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsTotalOrder_488 -> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.d_isPartialOrder_496
            ((T_TotalOrder_986 -> T_IsTotalOrder_488) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_TotalOrder_986 -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Bundles.d_isTotalOrder_1008
               (T_TotalOrder_986 -> AgdaAny
forall a b. a -> b
coe T_TotalOrder_986
v0))))
      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)