{-# 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.Irrelevant
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.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- 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._._.xs≮[]
d_xs'8814''91''93'_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] ->
  MAlonzo.Code.Data.List.Relation.Binary.Lex.Core.T_Lex_32 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_xs'8814''91''93'_38 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Lex_32
-> T_Irrelevant_20
d_xs'8814''91''93'_38 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.¬[]<[]
d_'172''91''93''60''91''93'_40 ::
  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.Irrelevant.T_Irrelevant_20
d_'172''91''93''60''91''93'_40 :: 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_Irrelevant_20
d_'172''91''93''60''91''93'_40 = 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_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-irreflexive
d_'60''45'irreflexive_42 ::
  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.Irrelevant.T_Irrelevant_20) ->
  [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.Irrelevant.T_Irrelevant_20
d_'60''45'irreflexive_42 :: 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Irrelevant_20
d_'60''45'irreflexive_42 = 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Pointwise_48
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-asymmetric
d_'60''45'asymmetric_60 ::
  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.Irrelevant.T_Irrelevant_20) ->
  [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.Irrelevant.T_Irrelevant_20
d_'60''45'asymmetric_60 :: 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Irrelevant_20
d_'60''45'asymmetric_60 = 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._.irrefl
d_irrefl_72 ::
  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.Irrelevant.T_Irrelevant_20) ->
  [AgdaAny] ->
  [AgdaAny] ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl_72 :: 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
d_irrefl_72 = 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._._.asym
d_asym_74 ::
  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.Irrelevant.T_Irrelevant_20) ->
  [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.Irrelevant.T_Irrelevant_20
d_asym_74 :: 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Irrelevant_20
d_asym_74 = 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_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Irrelevant_20
forall a. a
erased
-- Data.List.Relation.Binary.Lex.Strict._._.<-antisymmetric
d_'60''45'antisymmetric_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 ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [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_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 -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_'60''45'antisymmetric_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)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'60''45'antisymmetric_102
du_'60''45'antisymmetric_102 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [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_102 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'60''45'antisymmetric_102 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
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_104 ::
  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_28 ->
  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_104 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_'60''45'transitive_104 ~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_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'60''45'transitive_104
du_'60''45'transitive_104 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  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_104 :: T_IsEquivalence_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'60''45'transitive_104
  = (T_IsEquivalence_28
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> T_IsEquivalence_28
-> 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_28
-> 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_106 ::
  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_158) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
d_'60''45'compare_106 :: 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_158)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_158
d_'60''45'compare_106 ~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_158
v7 [AgdaAny]
v8 [AgdaAny]
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_158
du_'60''45'compare_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_158
v7 [AgdaAny]
v8 [AgdaAny]
v9
du_'60''45'compare_106 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158
du_'60''45'compare_106 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_158
du_'60''45'compare_106 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Tri_158
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_158) -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180
                    (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_158) -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172
                    (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_158
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_158) -> AgdaAny -> T_Tri_158
forall a b. a -> b
coe
                    AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188
                    (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 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T_Tri_158
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v8 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v9
                         -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172
                              ((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'_180 AgdaAny
v10
                         -> let v12 :: AgdaAny
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_158
du_'60''45'compare_106 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
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_158
forall a b. a -> b
coe AgdaAny
v12 of
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v13
                                   -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172
                                        ((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'_180 AgdaAny
v14
                                   -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180
                                        ((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'_188 AgdaAny
v15
                                   -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188
                                        ((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_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v11
                         -> (AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188
                              ((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_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             [AgdaAny]
_ -> T_Tri_158
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Tri_158
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Relation.Binary.Lex.Strict._._.<-decidable
d_'60''45'decidable_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 -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'60''45'decidable_274 :: 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_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_'60''45'decidable_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
  = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'60''45'decidable_274
du_'60''45'decidable_274 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'60''45'decidable_274 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'60''45'decidable_274
  = (T_Dec_20
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_20)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
forall a b. a -> b
coe
      T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_decidable_260
      ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
         (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
         (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
-- Data.List.Relation.Binary.Lex.Strict._._.<-respects₂
d_'60''45'respects'8322'_276 ::
  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_28 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'60''45'respects'8322'_276 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_Σ_14
-> T_Σ_14
d_'60''45'respects'8322'_276 ~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_28 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_276
du_'60''45'respects'8322'_276 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'60''45'respects'8322'_276 :: T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_276
  = (T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14)
-> T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      T_IsEquivalence_28 -> 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_278 ::
  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_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_370
-> T_IsStrictPartialOrder_370
d_'60''45'isStrictPartialOrder_278 ~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_370
v6
  = T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_278 T_IsStrictPartialOrder_370
v6
du_'60''45'isStrictPartialOrder_278 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_278 :: T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_278 T_IsStrictPartialOrder_370
v0
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.C_constructor_412
      ((T_IsEquivalence_28 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0)))
      ((T_IsEquivalence_28
 -> 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_28
-> 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_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0)))
      ((T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_respects'8322'_180
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.<-isStrictTotalOrder
d_'60''45'isStrictTotalOrder_314 ::
  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_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder_314 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_624
-> T_IsStrictTotalOrder_624
d_'60''45'isStrictTotalOrder_314 ~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_624
v6
  = T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_'60''45'isStrictTotalOrder_314 T_IsStrictTotalOrder_624
v6
du_'60''45'isStrictTotalOrder_314 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624
du_'60''45'isStrictTotalOrder_314 :: T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_'60''45'isStrictTotalOrder_314 T_IsStrictTotalOrder_624
v0
  = (T_IsStrictPartialOrder_370
 -> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Structures.C_constructor_680
      ((T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_278
         ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T_Tri_158
du_'60''45'compare_106
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
               ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
                  (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0))))
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
-- Data.List.Relation.Binary.Lex.Strict.<-strictPartialOrder
d_'60''45'strictPartialOrder_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_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_760
-> T_StrictPartialOrder_760
d_'60''45'strictPartialOrder_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_760
v3
  = T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_374 T_StrictPartialOrder_760
v3
du_'60''45'strictPartialOrder_374 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_374 :: T_StrictPartialOrder_760 -> T_StrictPartialOrder_760
du_'60''45'strictPartialOrder_374 T_StrictPartialOrder_760
v0
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      ((T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
du_'60''45'isStrictPartialOrder_278
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (T_StrictPartialOrder_760 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_760
v0)))
-- Data.List.Relation.Binary.Lex.Strict.<-strictTotalOrder
d_'60''45'strictTotalOrder_450 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder_450 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictTotalOrder_1280
d_'60''45'strictTotalOrder_450 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_'60''45'strictTotalOrder_450 T_StrictTotalOrder_1280
v3
du_'60''45'strictTotalOrder_450 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
du_'60''45'strictTotalOrder_450 :: T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_'60''45'strictTotalOrder_450 T_StrictTotalOrder_1280
v0
  = (T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280)
-> AgdaAny -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1386
      ((T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
du_'60''45'isStrictTotalOrder_314
         ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
            (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))
-- Data.List.Relation.Binary.Lex.Strict._.≤-reflexive
d_'8804''45'reflexive_560 ::
  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_560 :: 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_560 ~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_560 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v8
du_'8804''45'reflexive_560 ::
  [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_560 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_560 [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_560 ([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'__582 ::
  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'__582 :: 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'__582 = 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'__584 ::
  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'__584 :: 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'__584 = 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_586 ::
  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.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [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_586 :: 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_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
d_'8804''45'antisymmetric_586 ~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_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'8804''45'antisymmetric_586
du_'8804''45'antisymmetric_586 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [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_586 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Pointwise_48
du_'8804''45'antisymmetric_586 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
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_588 ::
  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_28 ->
  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_588 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
d_'8804''45'transitive_588 ~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_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'8804''45'transitive_588
du_'8804''45'transitive_588 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  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_588 :: T_IsEquivalence_28
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [AgdaAny]
-> [AgdaAny]
-> [AgdaAny]
-> T_Lex_32
-> T_Lex_32
-> T_Lex_32
du_'8804''45'transitive_588
  = (T_IsEquivalence_28
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [AgdaAny]
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Lex_32
 -> T_Lex_32
 -> T_Lex_32)
-> T_IsEquivalence_28
-> 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_28
-> 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_590 ::
  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_158) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_'8804''45'total_590 :: 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_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
d_'8804''45'total_590 ~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_158
v7 [AgdaAny]
v8 [AgdaAny]
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_590 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_158
v7 [AgdaAny]
v8 [AgdaAny]
v9
du_'8804''45'total_590 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_'8804''45'total_590 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_590 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T_Tri_158
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 :: AgdaAny
v8 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v1 AgdaAny
v4 AgdaAny
v6 in
                  AgdaAny -> T__'8846'__30
forall a b. a -> b
coe
                    (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
v8 of
                       MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 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'_180 AgdaAny
v10
                         -> let v12 :: AgdaAny
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_590 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) ((AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
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
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'_188 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_158
_ -> 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_694 ::
  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.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_'8804''45'decidable_694 :: 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_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
d_'8804''45'decidable_694 ~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_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'8804''45'decidable_694
du_'8804''45'decidable_694 ::
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  [AgdaAny] ->
  [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_'8804''45'decidable_694 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'8804''45'decidable_694
  = (T_Dec_20
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_20)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
forall a b. a -> b
coe
      T_Dec_20
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Lex.du_decidable_260
      ((Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
         (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
         ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.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'_696 ::
  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_28 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8804''45'respects'8322'_696 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> T_Σ_14
-> T_Σ_14
d_'8804''45'respects'8322'_696 ~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_28 -> T_Σ_14 -> T_Σ_14
du_'8804''45'respects'8322'_696
du_'8804''45'respects'8322'_696 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8804''45'respects'8322'_696 :: T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14
du_'8804''45'respects'8322'_696
  = (T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14)
-> T_IsEquivalence_28 -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      T_IsEquivalence_28 -> 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_698 ::
  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_28 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
d_'8804''45'isPreorder_698 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_76
d_'8804''45'isPreorder_698 ~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_28
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 T_Σ_14
v8
  = T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_76
du_'8804''45'isPreorder_698 T_IsEquivalence_28
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 T_Σ_14
v8
du_'8804''45'isPreorder_698 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_28 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_76
du_'8804''45'isPreorder_698 :: T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_76
du_'8804''45'isPreorder_698 T_IsEquivalence_28
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 T_Σ_14
v2
  = (T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsPreorder_76
forall a b. a -> b
coe
      T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Structures.C_constructor_126
      ((T_IsEquivalence_28 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28 -> T_IsEquivalence_28
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_isEquivalence_56
         (T_IsEquivalence_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_560)
      ((T_IsEquivalence_28
 -> 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_28
-> 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_28 -> AgdaAny
forall a b. a -> b
coe T_IsEquivalence_28
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_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_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
d_'8804''45'isPartialOrder_706 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_370
-> T_IsPartialOrder_248
d_'8804''45'isPartialOrder_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_IsStrictPartialOrder_370
v6
  = T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706 T_IsStrictPartialOrder_370
v6
du_'8804''45'isPartialOrder_706 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_370 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706 :: T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706 T_IsStrictPartialOrder_370
v0
  = (T_IsPreorder_76
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_248
forall a b. a -> b
coe
      T_IsPreorder_76
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_248
MAlonzo.Code.Relation.Binary.Structures.C_constructor_294
      ((T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_76
du_'8804''45'isPreorder_698
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386 (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
v0))
         ((T_IsStrictPartialOrder_370 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_388
            (T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_370
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_742 ::
  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_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
d_'8804''45'isDecPartialOrder_742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_624
-> T_IsDecPartialOrder_300
d_'8804''45'isDecPartialOrder_742 ~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_624
v6
  = T_IsStrictTotalOrder_624 -> T_IsDecPartialOrder_300
du_'8804''45'isDecPartialOrder_742 T_IsStrictTotalOrder_624
v6
du_'8804''45'isDecPartialOrder_742 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_300
du_'8804''45'isDecPartialOrder_742 :: T_IsStrictTotalOrder_624 -> T_IsDecPartialOrder_300
du_'8804''45'isDecPartialOrder_742 T_IsStrictTotalOrder_624
v0
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_300)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_300
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_300
MAlonzo.Code.Relation.Binary.Structures.C_constructor_364
      ((T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706
         ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__652 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'8804''45'decidable_694
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__652 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0))
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__654
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isTotalOrder
d_'8804''45'isTotalOrder_796 ::
  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_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
d_'8804''45'isTotalOrder_796 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_624
-> T_IsTotalOrder_488
d_'8804''45'isTotalOrder_796 ~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_624
v6
  = T_IsStrictTotalOrder_624 -> T_IsTotalOrder_488
du_'8804''45'isTotalOrder_796 T_IsStrictTotalOrder_624
v6
du_'8804''45'isTotalOrder_796 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_488
du_'8804''45'isTotalOrder_796 :: T_IsStrictTotalOrder_624 -> T_IsTotalOrder_488
du_'8804''45'isTotalOrder_796 T_IsStrictTotalOrder_624
v0
  = (T_IsPartialOrder_248
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_488
forall a b. a -> b
coe
      T_IsPartialOrder_248
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_488
MAlonzo.Code.Relation.Binary.Structures.C_constructor_540
      ((T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706
         ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_590
         ((T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
            ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
               ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
                  (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0))))
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_634 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isDecTotalOrder
d_'8804''45'isDecTotalOrder_850 ::
  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_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
d_'8804''45'isDecTotalOrder_850 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_624
-> T_IsDecTotalOrder_546
d_'8804''45'isDecTotalOrder_850 ~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_624
v6
  = T_IsStrictTotalOrder_624 -> T_IsDecTotalOrder_546
du_'8804''45'isDecTotalOrder_850 T_IsStrictTotalOrder_624
v6
du_'8804''45'isDecTotalOrder_850 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_624 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_546
du_'8804''45'isDecTotalOrder_850 :: T_IsStrictTotalOrder_624 -> T_IsDecTotalOrder_546
du_'8804''45'isDecTotalOrder_850 T_IsStrictTotalOrder_624
v0
  = (T_IsTotalOrder_488
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_546
forall a b. a -> b
coe
      T_IsTotalOrder_488
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_546
MAlonzo.Code.Relation.Binary.Structures.C_constructor_618
      ((T_IsStrictTotalOrder_624 -> T_IsTotalOrder_488)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624 -> T_IsTotalOrder_488
du_'8804''45'isTotalOrder_796 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny] -> [AgdaAny] -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny] -> [AgdaAny] -> T_Dec_20
MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__652 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
      (((AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'8804''45'decidable_694
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__652 (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0))
         ((T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__654
            (T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_624
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-preorder
d_'8804''45'preorder_910 ::
  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_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
d_'8804''45'preorder_910 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_142 -> T_Preorder_142
d_'8804''45'preorder_910 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_Preorder_142
v3
  = T_Preorder_142 -> T_Preorder_142
du_'8804''45'preorder_910 T_Preorder_142
v3
du_'8804''45'preorder_910 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_142
du_'8804''45'preorder_910 :: T_Preorder_142 -> T_Preorder_142
du_'8804''45'preorder_910 T_Preorder_142
v0
  = (T_IsPreorder_76 -> T_Preorder_142) -> AgdaAny -> T_Preorder_142
forall a b. a -> b
coe
      T_IsPreorder_76 -> T_Preorder_142
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_232
      ((T_IsEquivalence_28
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsPreorder_76)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_28
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_76
du_'8804''45'isPreorder_698
         ((T_IsPreorder_76 -> T_IsEquivalence_28) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_86
            ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)))
         ((T_IsPreorder_76
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_90
            ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0)))
         ((T_IsPreorder_76 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_76 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_124
            ((T_Preorder_142 -> T_IsPreorder_76) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_Preorder_142 -> T_IsPreorder_76
MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_164 (T_Preorder_142 -> AgdaAny
forall a b. a -> b
coe T_Preorder_142
v0))))
-- Data.List.Relation.Binary.Lex.Strict.≤-partialOrder
d_'8804''45'partialOrder_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_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
d_'8804''45'partialOrder_994 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_760
-> T_Poset_492
d_'8804''45'partialOrder_994 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_760
v3
  = T_StrictPartialOrder_760 -> T_Poset_492
du_'8804''45'partialOrder_994 T_StrictPartialOrder_760
v3
du_'8804''45'partialOrder_994 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_492
du_'8804''45'partialOrder_994 :: T_StrictPartialOrder_760 -> T_Poset_492
du_'8804''45'partialOrder_994 T_StrictPartialOrder_760
v0
  = (T_IsPartialOrder_248 -> T_Poset_492) -> AgdaAny -> T_Poset_492
forall a b. a -> b
coe
      T_IsPartialOrder_248 -> T_Poset_492
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_588
      ((T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsPartialOrder_248
du_'8804''45'isPartialOrder_706
         ((T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_760 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_782
            (T_StrictPartialOrder_760 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_760
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decPoset
d_'8804''45'decPoset_1070 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_596
d_'8804''45'decPoset_1070 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_DecPoset_596
d_'8804''45'decPoset_1070 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_DecPoset_596
du_'8804''45'decPoset_1070 T_StrictTotalOrder_1280
v3
du_'8804''45'decPoset_1070 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_596
du_'8804''45'decPoset_1070 :: T_StrictTotalOrder_1280 -> T_DecPoset_596
du_'8804''45'decPoset_1070 T_StrictTotalOrder_1280
v0
  = (T_IsDecPartialOrder_300 -> T_DecPoset_596)
-> AgdaAny -> T_DecPoset_596
forall a b. a -> b
coe
      T_IsDecPartialOrder_300 -> T_DecPoset_596
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_752
      ((T_IsStrictTotalOrder_624 -> T_IsDecPartialOrder_300)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624 -> T_IsDecPartialOrder_300
du_'8804''45'isDecPartialOrder_742
         ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
            (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decTotalOrder
d_'8804''45'decTotalOrder_1170 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
d_'8804''45'decTotalOrder_1170 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_DecTotalOrder_1098
d_'8804''45'decTotalOrder_1170 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_DecTotalOrder_1098
du_'8804''45'decTotalOrder_1170 T_StrictTotalOrder_1280
v3
du_'8804''45'decTotalOrder_1170 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_1098
du_'8804''45'decTotalOrder_1170 :: T_StrictTotalOrder_1280 -> T_DecTotalOrder_1098
du_'8804''45'decTotalOrder_1170 T_StrictTotalOrder_1280
v0
  = (T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098)
-> AgdaAny -> T_DecTotalOrder_1098
forall a b. a -> b
coe
      T_IsDecTotalOrder_546 -> T_DecTotalOrder_1098
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1272
      ((T_IsStrictTotalOrder_624 -> T_IsDecTotalOrder_546)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624 -> T_IsDecTotalOrder_546
du_'8804''45'isDecTotalOrder_850
         ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
            (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))