{-# 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_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_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_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_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_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_104
du_'60''45'transitive_104 ::
  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_104 :: 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_104
  = (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_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 :: t
v8 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> t
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
forall a. a
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 :: t
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T_Tri_158)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
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
forall a. a
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_26 ->
  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_26
-> 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_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_276
du_'60''45'respects'8322'_276 ::
  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'_276 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'60''45'respects'8322'_276
  = (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_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_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
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_290
-> T_IsStrictPartialOrder_290
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_290
v6
  = T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_278 T_IsStrictPartialOrder_290
v6
du_'60''45'isStrictPartialOrder_278 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_278 :: T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_278 T_IsStrictPartialOrder_290
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
      T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictPartialOrder'46'constructor_14045
      ((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_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
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_534
-> T_IsStrictTotalOrder_534
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_534
v6
  = T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder_314 T_IsStrictTotalOrder_534
v6
du_'60''45'isStrictTotalOrder_314 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder_314 :: T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder_314 T_IsStrictTotalOrder_534
v0
  = (T_IsStrictPartialOrder_290
 -> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290
-> (AgdaAny -> AgdaAny -> T_Tri_158) -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Structures.C_IsStrictTotalOrder'46'constructor_24953
      ((T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_278
         ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
            (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_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_IsStrictPartialOrder_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
               ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
                  (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0))))
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_556 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_556
-> T_StrictPartialOrder_556
d_'60''45'strictPartialOrder_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_556
v3
  = T_StrictPartialOrder_556 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_374 T_StrictPartialOrder_556
v3
du_'60''45'strictPartialOrder_374 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_374 :: T_StrictPartialOrder_556 -> T_StrictPartialOrder_556
du_'60''45'strictPartialOrder_374 T_StrictPartialOrder_556
v0
  = (T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556)
-> AgdaAny -> T_StrictPartialOrder_556
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
      ((T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
du_'60''45'isStrictPartialOrder_278
         ((T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_578
            (T_StrictPartialOrder_556 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_556
v0)))
-- Data.List.Relation.Binary.Lex.Strict.<-strictTotalOrder
d_'60''45'strictTotalOrder_442 ::
  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_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_442 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictTotalOrder_1036
d_'60''45'strictTotalOrder_442 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
  = T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_'60''45'strictTotalOrder_442 T_StrictTotalOrder_1036
v3
du_'60''45'strictTotalOrder_442 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
du_'60''45'strictTotalOrder_442 :: T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_'60''45'strictTotalOrder_442 T_StrictTotalOrder_1036
v0
  = (T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036)
-> AgdaAny -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
      T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_21059
      ((T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
du_'60''45'isStrictTotalOrder_314
         ((T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
            (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)))
-- Data.List.Relation.Binary.Lex.Strict._.≤-reflexive
d_'8804''45'reflexive_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] ->
  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_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_Pointwise_48
-> T_Lex_32
d_'8804''45'reflexive_544 ~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_544 [AgdaAny]
v6 [AgdaAny]
v7 T_Pointwise_48
v8
du_'8804''45'reflexive_544 ::
  [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_544 :: [AgdaAny] -> [AgdaAny] -> T_Pointwise_48 -> T_Lex_32
du_'8804''45'reflexive_544 [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_544 ([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'__566 ::
  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'__566 :: 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'__566 = 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'__568 ::
  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'__568 :: 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'__568 = 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_570 ::
  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_570 :: 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_570 ~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_570
du_'8804''45'antisymmetric_570 ::
  (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_570 :: (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_570 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_572 ::
  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_572 :: 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_572 ~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_572
du_'8804''45'transitive_572 ::
  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_572 :: 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_572
  = (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_574 ::
  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_574 :: 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_574 ~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_574 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T_Tri_158
v7 [AgdaAny]
v8 [AgdaAny]
v9
du_'8804''45'total_574 ::
  (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_574 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_574 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 :: t
v8 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> t
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
forall a. a
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 :: t
v12
                                  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T_Tri_158)
 -> [AgdaAny]
 -> [AgdaAny]
 -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> [AgdaAny]
-> [AgdaAny]
-> T__'8846'__30
du_'8804''45'total_574 ((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
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'_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_678 ::
  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_678 :: 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_678 ~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_678
du_'8804''45'decidable_678 ::
  (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_678 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> [AgdaAny]
-> [AgdaAny]
-> T_Dec_20
du_'8804''45'decidable_678
  = (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'_680 ::
  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'_680 :: 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'_680 ~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'_680
du_'8804''45'respects'8322'_680 ::
  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'_680 :: T_IsEquivalence_26 -> T_Σ_14 -> T_Σ_14
du_'8804''45'respects'8322'_680
  = (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_682 ::
  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_682 :: 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_682 ~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_682 T_IsEquivalence_26
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 T_Σ_14
v8
du_'8804''45'isPreorder_682 ::
  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_682 :: T_IsEquivalence_26
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> T_IsPreorder_70
du_'8804''45'isPreorder_682 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_4003
      ((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_544)
      ((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_690 ::
  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_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_'8804''45'isPartialOrder_690 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_290
-> T_IsPartialOrder_174
d_'8804''45'isPartialOrder_690 ~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_290
v6
  = T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690 T_IsStrictPartialOrder_290
v6
du_'8804''45'isPartialOrder_690 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690 :: T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690 T_IsStrictPartialOrder_290
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny -> T_IsPartialOrder_174
forall a b. a -> b
coe
      T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPartialOrder_174
MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
      ((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_682
         ((T_IsStrictPartialOrder_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306 (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
v0))
         ((T_IsStrictPartialOrder_290 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictPartialOrder_290 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.d_'60''45'resp'45''8776'_308
            (T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe T_IsStrictPartialOrder_290
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_726 ::
  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_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder_726 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_534
-> T_IsDecPartialOrder_224
d_'8804''45'isDecPartialOrder_726 ~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_534
v6
  = T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224
du_'8804''45'isDecPartialOrder_726 T_IsStrictTotalOrder_534
v6
du_'8804''45'isDecPartialOrder_726 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
du_'8804''45'isDecPartialOrder_726 :: T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224
du_'8804''45'isDecPartialOrder_726 T_IsStrictTotalOrder_534
v0
  = (T_IsPartialOrder_174
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecPartialOrder_224)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecPartialOrder_224
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecPartialOrder_224
MAlonzo.Code.Relation.Binary.Structures.C_IsDecPartialOrder'46'constructor_11683
      ((T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690
         ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
            (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__562 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_678
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__562 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0))
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__564
            (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isTotalOrder
d_'8804''45'isTotalOrder_780 ::
  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_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
d_'8804''45'isTotalOrder_780 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_534
-> T_IsTotalOrder_404
d_'8804''45'isTotalOrder_780 ~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_534
v6
  = T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404
du_'8804''45'isTotalOrder_780 T_IsStrictTotalOrder_534
v6
du_'8804''45'isTotalOrder_780 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
du_'8804''45'isTotalOrder_780 :: T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404
du_'8804''45'isTotalOrder_780 T_IsStrictTotalOrder_534
v0
  = (T_IsPartialOrder_174
 -> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_404)
-> AgdaAny -> AgdaAny -> T_IsTotalOrder_404
forall a b. a -> b
coe
      T_IsPartialOrder_174
-> (AgdaAny -> AgdaAny -> T__'8846'__30) -> T_IsTotalOrder_404
MAlonzo.Code.Relation.Binary.Structures.C_IsTotalOrder'46'constructor_20555
      ((T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690
         ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
            (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_574
         ((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_IsStrictPartialOrder_290 -> T_IsEquivalence_26)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictPartialOrder_290 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_302
               ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
                  (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0))))
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0)))
-- Data.List.Relation.Binary.Lex.Strict._._.≤-isDecTotalOrder
d_'8804''45'isDecTotalOrder_834 ::
  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_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder_834 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_534
-> T_IsDecTotalOrder_460
d_'8804''45'isDecTotalOrder_834 ~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_534
v6
  = T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
du_'8804''45'isDecTotalOrder_834 T_IsStrictTotalOrder_534
v6
du_'8804''45'isDecTotalOrder_834 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
du_'8804''45'isDecTotalOrder_834 :: T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
du_'8804''45'isDecTotalOrder_834 T_IsStrictTotalOrder_534
v0
  = (T_IsTotalOrder_404
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> T_Dec_20)
 -> T_IsDecTotalOrder_460)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_IsDecTotalOrder_460
forall a b. a -> b
coe
      T_IsTotalOrder_404
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> T_IsDecTotalOrder_460
MAlonzo.Code.Relation.Binary.Structures.C_IsDecTotalOrder'46'constructor_22695
      ((T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404
du_'8804''45'isTotalOrder_780 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__562 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
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_678
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'8799'__562 (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0))
         ((T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.du__'60''63'__564
            (T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe T_IsStrictTotalOrder_534
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-preorder
d_'8804''45'preorder_894 ::
  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_894 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_Preorder_132 -> T_Preorder_132
d_'8804''45'preorder_894 ~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_894 T_Preorder_132
v3
du_'8804''45'preorder_894 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
du_'8804''45'preorder_894 :: T_Preorder_132 -> T_Preorder_132
du_'8804''45'preorder_894 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_2267
      ((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_682
         ((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'_118
            ((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_970 ::
  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_556 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
d_'8804''45'partialOrder_970 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictPartialOrder_556
-> T_Poset_314
d_'8804''45'partialOrder_970 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictPartialOrder_556
v3
  = T_StrictPartialOrder_556 -> T_Poset_314
du_'8804''45'partialOrder_970 T_StrictPartialOrder_556
v3
du_'8804''45'partialOrder_970 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
du_'8804''45'partialOrder_970 :: T_StrictPartialOrder_556 -> T_Poset_314
du_'8804''45'partialOrder_970 T_StrictPartialOrder_556
v0
  = (T_IsPartialOrder_174 -> T_Poset_314) -> AgdaAny -> T_Poset_314
forall a b. a -> b
coe
      T_IsPartialOrder_174 -> T_Poset_314
MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
      ((T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_'8804''45'isPartialOrder_690
         ((T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictPartialOrder_556 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_578
            (T_StrictPartialOrder_556 -> AgdaAny
forall a b. a -> b
coe T_StrictPartialOrder_556
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decPoset
d_'8804''45'decPoset_1038 ::
  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_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_406
d_'8804''45'decPoset_1038 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_DecPoset_406
d_'8804''45'decPoset_1038 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
  = T_StrictTotalOrder_1036 -> T_DecPoset_406
du_'8804''45'decPoset_1038 T_StrictTotalOrder_1036
v3
du_'8804''45'decPoset_1038 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecPoset_406
du_'8804''45'decPoset_1038 :: T_StrictTotalOrder_1036 -> T_DecPoset_406
du_'8804''45'decPoset_1038 T_StrictTotalOrder_1036
v0
  = (T_IsDecPartialOrder_224 -> T_DecPoset_406)
-> AgdaAny -> T_DecPoset_406
forall a b. a -> b
coe
      T_IsDecPartialOrder_224 -> T_DecPoset_406
MAlonzo.Code.Relation.Binary.Bundles.C_DecPoset'46'constructor_8213
      ((T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsDecPartialOrder_224
du_'8804''45'isDecPartialOrder_726
         ((T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
            (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)))
-- Data.List.Relation.Binary.Lex.Strict.≤-decTotalOrder
d_'8804''45'decTotalOrder_1130 ::
  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_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
d_'8804''45'decTotalOrder_1130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_DecTotalOrder_866
d_'8804''45'decTotalOrder_1130 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
  = T_StrictTotalOrder_1036 -> T_DecTotalOrder_866
du_'8804''45'decTotalOrder_1130 T_StrictTotalOrder_1036
v3
du_'8804''45'decTotalOrder_1130 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_DecTotalOrder_866
du_'8804''45'decTotalOrder_1130 :: T_StrictTotalOrder_1036 -> T_DecTotalOrder_866
du_'8804''45'decTotalOrder_1130 T_StrictTotalOrder_1036
v0
  = (T_IsDecTotalOrder_460 -> T_DecTotalOrder_866)
-> AgdaAny -> T_DecTotalOrder_866
forall a b. a -> b
coe
      T_IsDecTotalOrder_460 -> T_DecTotalOrder_866
MAlonzo.Code.Relation.Binary.Bundles.C_DecTotalOrder'46'constructor_17849
      ((T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
du_'8804''45'isDecTotalOrder_834
         ((T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
            (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)))