{-# 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.Relation.Binary.Lex.Strict 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.Bool
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.List.Relation.Binary.Lex
import qualified MAlonzo.Code.Data.List.Relation.Binary.Lex.Core
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base
import qualified MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Consequences
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary

-- Data.List.Relation.Binary.Lex.Strict._._._≋_
d__'8779'__32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'8779'__32 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'8779'__32 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._<_
d__'60'__34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'60'__34 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'60'__34 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.¬[]<[]
d_'172''91''93''60''91''93'_36 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'172''91''93''60''91''93'_36 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Lex_32
-> T_'8869'_4
d_'172''91''93''60''91''93'_36 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Lex_32
-> T_'8869'_4
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-irreflexive
d_'60''45'irreflexive_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''45'irreflexive_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_'8869'_4
d_'60''45'irreflexive_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_'8869'_4
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-asymmetric
d_'60''45'asymmetric_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'60''45'asymmetric_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_'8869'_4
d_'60''45'asymmetric_56 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_'8869'_4
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._.irrefl
d_irrefl_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_irrefl_68 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._.asym
d_asym_70 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym_70 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_'8869'_4
d_asym_70 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_'8869'_4
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-antisymmetric
d_'60''45'antisymmetric_98 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'60''45'antisymmetric_98 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_'60''45'antisymmetric_98 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'60''45'antisymmetric_98
du_'60''45'antisymmetric_98 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'60''45'antisymmetric_98 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'60''45'antisymmetric_98 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
v2 [AgdaAny]
v3 [AgdaAny]
v4
  = ([AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48)
-> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_antisymmetric_78 [AgdaAny]
v3
      [AgdaAny]
v4
-- Data.List.Relation.Binary.Lex.Strict._._.<-transitive
d_'60''45'transitive_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_'60''45'transitive_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_'60''45'transitive_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'60''45'transitive_100
du_'60''45'transitive_100 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_'60''45'transitive_100 :: T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'60''45'transitive_100
  = (T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
forall a b. a -> b
coe T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_transitive_132
-- Data.List.Relation.Binary.Lex.Strict._._.<-compare
d_'60''45'compare_102 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
d_'60''45'compare_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_136
d_'60''45'compare_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_136
v7 [AgdaAny]
v8 [AgdaAny]
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_136
du_'60''45'compare_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_136
v7 [AgdaAny]
v8 [AgdaAny]
v9
du_'60''45'compare_102 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136
du_'60''45'compare_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_136
du_'60''45'compare_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Tri_136
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158
                    (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe
                       T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
             (:) AgdaAny
v4 [AgdaAny]
v5
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                    (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48)
             [AgdaAny]
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T_Tri_136) -> AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                    (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48)
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: t
v8 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_Tri_136
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v9
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                              ((AgdaAny -> T_Lex_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v9)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v10
                         -> let v12 :: t
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Tri_136)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_136
du_'60''45'compare_102 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v13
                                   -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150
                                        ((AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                           AgdaAny
v10 AgdaAny
v13)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v14
                                   -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158
                                        ((AgdaAny -> T_Pointwise_48 -> T_Pointwise_48)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Pointwise_48 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                           AgdaAny
v10 AgdaAny
v14)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v15
                                   -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                                        ((AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                           ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v6 AgdaAny
v10) AgdaAny
v15)
                                 T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v11
                         -> (AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166
                              ((AgdaAny -> T_Lex_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v11)
                       T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Tri_136
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex.Strict._._.<-decidable
d_'60''45'decidable_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'60''45'decidable_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
d_'60''45'decidable_270 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'60''45'decidable_270
du_'60''45'decidable_270 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'60''45'decidable_270 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'60''45'decidable_270
  = (T_Dec_32
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_32)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
forall a b. a -> b
coe
      T_Dec_32
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_decidable_260
      ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
         (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
         (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26))
-- Data.List.Relation.Binary.Lex.Strict._._.<-respects₂
d_'60''45'respects'8322'_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'respects'8322'_272 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> T_Σ_14
d_'60''45'respects'8322'_272 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_272
du_'60''45'respects'8322'_272 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'respects'8322'_272 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_272
  = (T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14)
-> T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_respects'8322'_180
-- Data.List.Relation.Binary.Lex.Strict._._.<-isStrictPartialOrder
d_'60''45'isStrictPartialOrder_274 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_274 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_266
-> T_IsStrictPartialOrder_266
d_'60''45'isStrictPartialOrder_274 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictPartialOrder_266
v6
  = T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_274 T_IsStrictPartialOrder_266
v6
du_'60''45'isStrictPartialOrder_274 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_274 :: T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_274 T_IsStrictPartialOrder_266
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_266
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_13145
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
         ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      ((T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_transitive_132
         ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
         ((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
         ((T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      ((T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_respects'8322'_180
         ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
         ((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.<-isStrictTotalOrder
d_'60''45'isStrictTotalOrder_312 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder_312 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsStrictTotalOrder_502
d_'60''45'isStrictTotalOrder_312 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictTotalOrder_502
v6
  = T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''45'isStrictTotalOrder_312 T_IsStrictTotalOrder_502
v6
du_'60''45'isStrictTotalOrder_312 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502
du_'60''45'isStrictTotalOrder_312 :: T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''45'isStrictTotalOrder_312 T_IsStrictTotalOrder_502
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_23999
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
         ((T_IsStrictTotalOrder_502 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_512
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      ((T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> T_IsEquivalence_26
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'60''45'transitive_100
         (T_IsStrictTotalOrder_502 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_512
            (T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
         (((AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14
MAlonzo.Code.Relation.Binary.Consequences.du_trans'8743'tri'8658'resp_650
            ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
         (T_IsStrictTotalOrder_502
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_514 (T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Tri_136)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_136
du_'60''45'compare_102
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            ((T_IsStrictTotalOrder_502 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictTotalOrder_502 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_512
               (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Data.List.Relation.Binary.Lex.Strict.<-strictPartialOrder
d_'60''45'strictPartialOrder_370 ::
  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_StrictPartialOrder_472 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_370 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_472
-> T_StrictPartialOrder_472
d_'60''45'strictPartialOrder_370 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_472
v3
  = T_StrictPartialOrder_472 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_370 T_StrictPartialOrder_472
v3
du_'60''45'strictPartialOrder_370 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_370 :: T_StrictPartialOrder_472 -> T_StrictPartialOrder_472
du_'60''45'strictPartialOrder_370 T_StrictPartialOrder_472
v0
  = (T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_8957
      ((T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
du_'60''45'isStrictPartialOrder_274
         ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
            (T_StrictPartialOrder_472 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_472
v0)))
-- Data.List.Relation.Binary.Lex.Strict.<-strictTotalOrder
d_'60''45'strictTotalOrder_434 ::
  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_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_'60''45'strictTotalOrder_434 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictTotalOrder_864
d_'60''45'strictTotalOrder_434 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
  = T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_'60''45'strictTotalOrder_434 T_StrictTotalOrder_864
v3
du_'60''45'strictTotalOrder_434 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
du_'60''45'strictTotalOrder_434 :: T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_'60''45'strictTotalOrder_434 T_StrictTotalOrder_864
v0
  = (T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864)
-> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_16739
      ((T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
du_'60''45'isStrictTotalOrder_312
         ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))
-- Data.List.Relation.Binary.Lex.Strict._.≤-reflexive
d_'8804''45'reflexive_522 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_'8804''45'reflexive_522 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
d_'8804''45'reflexive_522 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v8
  = [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_522 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v8
du_'8804''45'reflexive_522 ::
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_'8804''45'reflexive_522 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_522 [AgdaAny]
v0 [AgdaAny]
v1 T_Pointwise_48
v2
  = case T_Pointwise_48 -> T_Pointwise_48
forall a b. a -> b
coe T_Pointwise_48
v2 of
      T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        -> (AgdaAny -> T_Lex_32) -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
             AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42
             (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)
      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 AgdaAny
v7 T_Pointwise_48
v8
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v0 of
             (:) AgdaAny
v9 [AgdaAny]
v10
               -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v1 of
                    (:) AgdaAny
v11 [AgdaAny]
v12
                      -> (AgdaAny -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> T_Lex_32
forall a b. a -> b
coe
                           AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74 AgdaAny
v7
                           (([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_522 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v10) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v12) (T_Pointwise_48 -> AgdaAny
forall a b. a -> b
coe T_Pointwise_48
v8))
                    [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
             [AgdaAny]
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pointwise_48
_ -> T_Lex_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex.Strict._._._≋_
d__'8779'__544 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'8779'__544 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'8779'__544 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._≤_
d__'8804'__546 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) -> [AgdaAny] -> [AgdaAny] -> ()
d__'8804'__546 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
d__'8804'__546 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> [AgdaAny]
-> T_Level_18
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.≤-antisymmetric
d_'8804''45'antisymmetric_548 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
d_'8804''45'antisymmetric_548 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_'8804''45'antisymmetric_548 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'8804''45'antisymmetric_548
du_'8804''45'antisymmetric_548 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
du_'8804''45'antisymmetric_548 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'8804''45'antisymmetric_548 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4
v2 [AgdaAny]
v3 [AgdaAny]
v4
  = ([AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48)
-> [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
forall a b. a -> b
coe
      [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_antisymmetric_78 [AgdaAny]
v3
      [AgdaAny]
v4
-- Data.List.Relation.Binary.Lex.Strict._._.≤-transitive
d_'8804''45'transitive_550 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
d_'8804''45'transitive_550 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_'8804''45'transitive_550 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'8804''45'transitive_550
du_'8804''45'transitive_550 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [AgdaAny] ->
  [AgdaAny] ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32
du_'8804''45'transitive_550 :: T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'8804''45'transitive_550
  = (T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
forall a b. a -> b
coe T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_transitive_132
-- Data.List.Relation.Binary.Lex.Strict._._.≤-total
d_'8804''45'total_552 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8804''45'total_552 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
d_'8804''45'total_552 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_136
v7 [AgdaAny]
v8 [AgdaAny]
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_552 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_136
v7 [AgdaAny]
v8 [AgdaAny]
v9
du_'8804''45'total_552 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8804''45'total_552 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_552 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Tri_136
v1 [AgdaAny]
v2 [AgdaAny]
v3
  = case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v2 of
      []
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                    ((AgdaAny -> T_Lex_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_base_42
                       (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
             (:) AgdaAny
v4 [AgdaAny]
v5
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                    (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48)
             [AgdaAny]
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> case [AgdaAny] -> [AgdaAny]
forall a b. a -> b
coe [AgdaAny]
v3 of
             []
               -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                    (T_Lex_32 -> AgdaAny
forall a b. a -> b
coe T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_halt_48)
             (:) AgdaAny
v6 [AgdaAny]
v7
               -> let v8 :: t
v8 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v9
                         -> (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 -> T_Lex_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v9)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v10
                         -> let v12 :: t
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_552 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v1) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7) in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v13
                                   -> (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 -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                           AgdaAny
v10 AgdaAny
v13)
                                 MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v13
                                   -> (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 -> T_Lex_32 -> T_Lex_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> T_Lex_32 -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_next_74
                                           ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v4 AgdaAny
v6 AgdaAny
v10) AgdaAny
v13)
                                 T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v11
                         -> (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 -> T_Lex_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.C_this_60 AgdaAny
v11)
                       T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex.Strict._._.≤-decidable
d_'8804''45'decidable_656 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8804''45'decidable_656 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
d_'8804''45'decidable_656 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'8804''45'decidable_656
du_'8804''45'decidable_656 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8804''45'decidable_656 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'8804''45'decidable_656
  = (T_Dec_32
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_32)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
forall a b. a -> b
coe
      T_Dec_32
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_decidable_260
      ((Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
         (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
         ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
            (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-respects₂
d_'8804''45'respects'8322'_658 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''45'respects'8322'_658 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> T_Σ_14
-> T_Σ_14
d_'8804''45'respects'8322'_658 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5
  = T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'8804''45'respects'8322'_658
du_'8804''45'respects'8322'_658 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''45'respects'8322'_658 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'8804''45'respects'8322'_658
  = (T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14)
-> T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_respects'8322'_180
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isPreorder
d_'8804''45'isPreorder_660 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
d_'8804''45'isPreorder_660 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
d_'8804''45'isPreorder_660 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsEquivalence_26
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 T_Σ_14
v8
  = T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
du_'8804''45'isPreorder_660 T_IsEquivalence_26
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 T_Σ_14
v8
du_'8804''45'isPreorder_660 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_'8804''45'isPreorder_660 :: T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
du_'8804''45'isPreorder_660 T_IsEquivalence_26
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_70
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_3993
      ((T_IsEquivalence_26 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> T_IsEquivalence_26
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0))
      (([AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_522)
      ((T_IsEquivalence_26
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_transitive_132
         (T_IsEquivalence_26 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_26
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isPartialOrder
d_'8804''45'isPartialOrder_668 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
d_'8804''45'isPartialOrder_668 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_266
-> T_IsPartialOrder_162
d_'8804''45'isPartialOrder_668 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictPartialOrder_266
v6
  = T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668 T_IsStrictPartialOrder_266
v6
du_'8804''45'isPartialOrder_668 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_266 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668 :: T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668 T_IsStrictPartialOrder_266
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_162
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_162
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9297
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
du_'8804''45'isPreorder_660
         ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
         ((T_IsStrictPartialOrder_266
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_282 (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0))
         ((T_IsStrictPartialOrder_266 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_266 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_284
            (T_IsStrictPartialOrder_266 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_266
v0)))
      (([AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48)
-> AgdaAny
forall a b. a -> b
coe
         [AgdaAny] -> [AgdaAny] -> T_Lex_32 -> T_Lex_32 -> T_Pointwise_48
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_antisymmetric_78)
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isDecPartialOrder
d_'8804''45'isDecPartialOrder_706 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
d_'8804''45'isDecPartialOrder_706 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsDecPartialOrder_206
d_'8804''45'isDecPartialOrder_706 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictTotalOrder_502
v6
  = T_IsStrictTotalOrder_502 -> T_IsDecPartialOrder_206
du_'8804''45'isDecPartialOrder_706 T_IsStrictTotalOrder_502
v6
du_'8804''45'isDecPartialOrder_706 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_206
du_'8804''45'isDecPartialOrder_706 :: T_IsStrictTotalOrder_502 -> T_IsDecPartialOrder_206
du_'8804''45'isDecPartialOrder_706 T_IsStrictTotalOrder_502
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_206
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecPartialOrder_206
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_10957
      ((T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668
         ((T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.du_isStrictPartialOrder_540
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'8804''45'decidable_656
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__520
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isTotalOrder
d_'8804''45'isTotalOrder_758 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
d_'8804''45'isTotalOrder_758 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsTotalOrder_384
d_'8804''45'isTotalOrder_758 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictTotalOrder_502
v6
  = T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_'8804''45'isTotalOrder_758 T_IsStrictTotalOrder_502
v6
du_'8804''45'isTotalOrder_758 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_384
du_'8804''45'isTotalOrder_758 :: T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_'8804''45'isTotalOrder_758 T_IsStrictTotalOrder_502
v0
  = (T_IsPartialOrder_162
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_384
forall a b. a -> b
coe
      T_IsPartialOrder_162
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_384
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_19815
      ((T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668
         ((T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.du_isStrictPartialOrder_540
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_136)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_552
         ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
            ((T_IsStrictTotalOrder_502 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictTotalOrder_502 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_512
               (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Tri_136
MAlonzo.Code.Relation.Binary.Structures.d_compare_516 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isDecTotalOrder
d_'8804''45'isDecTotalOrder_810 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
d_'8804''45'isDecTotalOrder_810 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_502
-> T_IsDecTotalOrder_434
d_'8804''45'isDecTotalOrder_810 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 T_IsStrictTotalOrder_502
v6
  = T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434
du_'8804''45'isDecTotalOrder_810 T_IsStrictTotalOrder_502
v6
du_'8804''45'isDecTotalOrder_810 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_502 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_434
du_'8804''45'isDecTotalOrder_810 :: T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434
du_'8804''45'isDecTotalOrder_810 T_IsStrictTotalOrder_502
v0
  = (T_IsTotalOrder_384
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_434
forall a b. a -> b
coe
      T_IsTotalOrder_384
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> T_IsDecTotalOrder_434
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_21785
      ((T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502 -> T_IsTotalOrder_384
du_'8804''45'isTotalOrder_758 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_32
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_32)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_32
du_'8804''45'decidable_656
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__518 (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0))
         ((T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> AgdaAny -> AgdaAny -> T_Dec_32
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__520
            (T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_502
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-preorder
d_'8804''45'preorder_868 ::
  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_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
d_'8804''45'preorder_868 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_'8804''45'preorder_868 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_132
v3
  = T_Preorder_132 -> T_Preorder_132
du_'8804''45'preorder_868 T_Preorder_132
v3
du_'8804''45'preorder_868 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_'8804''45'preorder_868 :: T_Preorder_132 -> T_Preorder_132
du_'8804''45'preorder_868 T_Preorder_132
v0
  = (T_IsPreorder_70 -> T_Preorder_132) -> AgdaAny -> T_Preorder_132
forall a b. a -> b
coe
      T_IsPreorder_70 -> T_Preorder_132
MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2269
      ((T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
du_'8804''45'isPreorder_660
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
         ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0)))
         ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_112
            ((T_Preorder_132 -> T_IsPreorder_70) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_132 -> T_IsPreorder_70
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (T_Preorder_132 -> AgdaAny
forall a b. a -> b
coe T_Preorder_132
v0))))
-- Data.List.Relation.Binary.Lex.Strict.≤-partialOrder
d_'8804''45'partialOrder_930 ::
  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_StrictPartialOrder_472 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
d_'8804''45'partialOrder_930 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_472
-> T_Poset_282
d_'8804''45'partialOrder_930 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_472
v3
  = T_StrictPartialOrder_472 -> T_Poset_282
du_'8804''45'partialOrder_930 T_StrictPartialOrder_472
v3
du_'8804''45'partialOrder_930 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_282
du_'8804''45'partialOrder_930 :: T_StrictPartialOrder_472 -> T_Poset_282
du_'8804''45'partialOrder_930 T_StrictPartialOrder_472
v0
  = (T_IsPartialOrder_162 -> T_Poset_282) -> AgdaAny -> T_Poset_282
forall a b. a -> b
coe
      T_IsPartialOrder_162 -> T_Poset_282
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_5219
      ((T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsPartialOrder_162
du_'8804''45'isPartialOrder_668
         ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
            (T_StrictPartialOrder_472 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_472
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decPoset
d_'8804''45'decPoset_994 ::
  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_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
d_'8804''45'decPoset_994 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_DecPoset_360
d_'8804''45'decPoset_994 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
  = T_StrictTotalOrder_864 -> T_DecPoset_360
du_'8804''45'decPoset_994 T_StrictTotalOrder_864
v3
du_'8804''45'decPoset_994 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_360
du_'8804''45'decPoset_994 :: T_StrictTotalOrder_864 -> T_DecPoset_360
du_'8804''45'decPoset_994 T_StrictTotalOrder_864
v0
  = (T_IsDecPartialOrder_206 -> T_DecPoset_360)
-> AgdaAny -> T_DecPoset_360
forall a b. a -> b
coe
      T_IsDecPartialOrder_206 -> T_DecPoset_360
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_6777
      ((T_IsStrictTotalOrder_502 -> T_IsDecPartialOrder_206)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502 -> T_IsDecPartialOrder_206
du_'8804''45'isDecPartialOrder_706
         ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decTotalOrder
d_'8804''45'decTotalOrder_1072 ::
  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_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
d_'8804''45'decTotalOrder_1072 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_DecTotalOrder_740
d_'8804''45'decTotalOrder_1072 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
  = T_StrictTotalOrder_864 -> T_DecTotalOrder_740
du_'8804''45'decTotalOrder_1072 T_StrictTotalOrder_864
v3
du_'8804''45'decTotalOrder_1072 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_740
du_'8804''45'decTotalOrder_1072 :: T_StrictTotalOrder_864 -> T_DecTotalOrder_740
du_'8804''45'decTotalOrder_1072 T_StrictTotalOrder_864
v0
  = (T_IsDecTotalOrder_434 -> T_DecTotalOrder_740)
-> AgdaAny -> T_DecTotalOrder_740
forall a b. a -> b
coe
      T_IsDecTotalOrder_434 -> T_DecTotalOrder_740
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_14337
      ((T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502 -> T_IsDecTotalOrder_434
du_'8804''45'isDecTotalOrder_810
         ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))