{-# 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.Relation.Binary.Consequences 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.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Empty.Irrelevant
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Binary.Consequences._.subst⇒respˡ
d_subst'8658'resp'737'_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_subst'8658'resp'737'_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_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subst'8658'resp'737'_38 ~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 -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
                          AgdaAny
v11
  = (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'737'_38 AgdaAny -> AgdaAny -> T_Level_18
v5 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_subst'8658'resp'737'_38 ::
  (AgdaAny -> AgdaAny -> ()) ->
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_subst'8658'resp'737'_38 :: (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'737'_38 AgdaAny -> AgdaAny -> T_Level_18
v0 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 (\ AgdaAny
v7 -> (AgdaAny -> AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Level_18
v0 AgdaAny
v7 AgdaAny
v2) AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
-- Relation.Binary.Consequences._.subst⇒respʳ
d_subst'8658'resp'691'_48 ::
  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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_subst'8658'resp'691'_48 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subst'8658'resp'691'_48 ~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 -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
                          AgdaAny
v11
  = (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'691'_48 AgdaAny -> AgdaAny -> T_Level_18
v5 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_subst'8658'resp'691'_48 ::
  (AgdaAny -> AgdaAny -> ()) ->
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_subst'8658'resp'691'_48 :: (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'691'_48 AgdaAny -> AgdaAny -> T_Level_18
v0 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
  = ((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 ((AgdaAny -> AgdaAny -> T_Level_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Level_18
v0 AgdaAny
v2) AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6
-- Relation.Binary.Consequences._.subst⇒resp₂
d_subst'8658'resp'8322'_58 ::
  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.Agda.Builtin.Sigma.T_Σ_14
d_subst'8658'resp'8322'_58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_subst'8658'resp'8322'_58 ~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 -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
  = ((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_subst'8658'resp'8322'_58 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
du_subst'8658'resp'8322'_58 ::
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_subst'8658'resp'8322'_58 :: ((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_subst'8658'resp'8322'_58 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (((AgdaAny -> AgdaAny -> T_Level_18)
 -> ((AgdaAny -> T_Level_18)
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'691'_48 AgdaAny
forall a. a
erased (((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0))
      (((AgdaAny -> AgdaAny -> T_Level_18)
 -> ((AgdaAny -> T_Level_18)
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'737'_38 AgdaAny
forall a. a
erased (((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0))
-- Relation.Binary.Consequences._.resp⇒¬-resp
d_resp'8658''172''45'resp_76 ::
  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) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_resp'8658''172''45'resp_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_resp'8658''172''45'resp_76 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.total⇒refl
d_total'8658'refl_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 -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_total'8658'refl_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_total'8658'refl_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 T_Σ_14
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_total'8658'refl_102 T_Σ_14
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
du_total'8658'refl_102 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_total'8658'refl_102 :: T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_total'8658'refl_102 T_Σ_14
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v0 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
        -> let v8 :: t
v8 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v2 AgdaAny
v3 AgdaAny
v4 in
           AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v8 of
                MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9
                MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
                  -> AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6 AgdaAny
v3 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 (AgdaAny
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7 AgdaAny
v3 AgdaAny
v4 AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5) AgdaAny
v9)
                T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Consequences._.total∧dec⇒dec
d_total'8743'dec'8658'dec_154 ::
  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 -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_total'8743'dec'8658'dec_154 :: 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 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_total'8743'dec'8658'dec_154 ~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 -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9
                              AgdaAny
v10 AgdaAny
v11
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_total'8743'dec'8658'dec_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9 AgdaAny
v10 AgdaAny
v11
du_total'8743'dec'8658'dec_154 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_total'8743'dec'8658'dec_154 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_total'8743'dec'8658'dec_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny
v3 AgdaAny
v4
  = let v5 :: t
v5 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v1 AgdaAny
v3 AgdaAny
v4 in
    AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v6
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v6
           -> ((AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny) -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v3 AgdaAny
v4) ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v2 AgdaAny
v3 AgdaAny
v4)
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.mono⇒cong
d_mono'8658'cong_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_mono'8658'cong_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> 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)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_mono'8658'cong_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9 ~AgdaAny -> AgdaAny -> T_Level_18
v10
                     ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 AgdaAny
v19
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 AgdaAny
v19
du_mono'8658'cong_226 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_mono'8658'cong_226 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_mono'8658'cong_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v3
         (\ AgdaAny
v8 AgdaAny
v9 -> AgdaAny
v8) AgdaAny
v5 AgdaAny
v6)
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v8 AgdaAny
v9 -> AgdaAny
v9) AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v6)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6 AgdaAny
v5 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v6 AgdaAny
v5 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7)))
-- Relation.Binary.Consequences._.antimono⇒cong
d_antimono'8658'cong_240 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_antimono'8658'cong_240 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> 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)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_antimono'8658'cong_240 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~AgdaAny -> AgdaAny -> T_Level_18
v8 ~AgdaAny -> AgdaAny -> T_Level_18
v9
                         ~AgdaAny -> AgdaAny -> T_Level_18
v10 ~AgdaAny -> AgdaAny -> T_Level_18
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 AgdaAny
v19
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_240 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny -> AgdaAny
v15 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 AgdaAny
v19
du_antimono'8658'cong_240 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_antimono'8658'cong_240 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_antimono'8658'cong_240 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny -> AgdaAny
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
      (((AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du_'8739'_'10217''45'__308
         (\ AgdaAny
v8 AgdaAny
v9 -> AgdaAny
v9) AgdaAny -> AgdaAny
v3 AgdaAny
v6 AgdaAny
v5)
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'45''10216'_'8739'_302 AgdaAny -> AgdaAny
v3
         (\ AgdaAny
v8 AgdaAny
v9 -> AgdaAny
v8) AgdaAny
v6 AgdaAny
v5)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v6 AgdaAny
v5 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v6 AgdaAny
v5 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7)))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7))
-- Relation.Binary.Consequences._.trans∧irr⇒asym
d_trans'8743'irr'8658'asym_266 ::
  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) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_trans'8743'irr'8658'asym_266 :: 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)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_trans'8743'irr'8658'asym_266 = 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)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.irr∧antisym⇒asym
d_irr'8743'antisym'8658'asym_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 -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irr'8743'antisym'8658'asym_278 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_irr'8743'antisym'8658'asym_278 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.asym⇒antisym
d_asym'8658'antisym_288 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_asym'8658'antisym_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_asym'8658'antisym_288 ~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 -> T_'8869'_4
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                        ~AgdaAny
v10
  = AgdaAny
du_asym'8658'antisym_288
du_asym'8658'antisym_288 :: AgdaAny
du_asym'8658'antisym_288 :: AgdaAny
du_asym'8658'antisym_288
  = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10
-- Relation.Binary.Consequences._.asym⇒irr
d_asym'8658'irr_296 ::
  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.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym'8658'irr_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asym'8658'irr_296 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.tri⇒asym
d_tri'8658'asym_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 -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_tri'8658'asym_314 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_tri'8658'asym_314 = 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.tri⇒irr
d_tri'8658'irr_366 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_tri'8658'irr_366 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_tri'8658'irr_366 = 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences._.tri⇒dec≈
d_tri'8658'dec'8776'_426 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_tri'8658'dec'8776'_426 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_tri'8658'dec'8776'_426 ~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_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'8776'_426 AgdaAny -> AgdaAny -> T_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
du_tri'8658'dec'8776'_426 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_tri'8658'dec'8776'_426 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'8776'_426 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.tri⇒dec<
d_tri'8658'dec'60'_462 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_tri'8658'dec'60'_462 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_tri'8658'dec'60'_462 ~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_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'60'_462 AgdaAny -> AgdaAny -> T_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
du_tri'8658'dec'60'_462 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_tri'8658'dec'60'_462 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'60'_462 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
                (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.trans∧tri⇒respʳ
d_trans'8743'tri'8658'resp'691'_498 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans'8743'tri'8658'resp'691'_498 :: 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 -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans'8743'tri'8658'resp'691'_498 ~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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
                                    ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 ~AgdaAny
v11 AgdaAny
v12 ~AgdaAny
v13 ~AgdaAny
v14
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'691'_498 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 AgdaAny
v12
du_trans'8743'tri'8658'resp'691'_498 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'691'_498 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'691'_498 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.trans∧tri⇒respˡ
d_trans'8743'tri'8658'resp'737'_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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans'8743'tri'8658'resp'737'_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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans'8743'tri'8658'resp'737'_582 ~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
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
                                    AgdaAny -> AgdaAny -> T_Tri_136
v8 AgdaAny
v9 ~AgdaAny
v10 AgdaAny
v11 ~AgdaAny
v12 ~AgdaAny
v13
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'737'_582 AgdaAny -> AgdaAny -> T_Tri_136
v8 AgdaAny
v9 AgdaAny
v11
du_trans'8743'tri'8658'resp'737'_582 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'737'_582 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'737'_582 AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0 AgdaAny
v2 AgdaAny
v1 in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_136
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_150 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_158 AgdaAny
v5
           -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_166 AgdaAny
v6
           -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
MAlonzo.Code.Data.Empty.Irrelevant.du_'8869''45'elim_10
         T_Tri_136
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.trans∧tri⇒resp
d_trans'8743'tri'8658'resp_650 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_trans'8743'tri'8658'resp_650 :: 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 -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> T_Σ_14
d_trans'8743'tri'8658'resp_650 ~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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8
                               AgdaAny -> AgdaAny -> T_Tri_136
v9
  = (AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14
du_trans'8743'tri'8658'resp_650 AgdaAny -> AgdaAny -> T_Tri_136
v9
du_trans'8743'tri'8658'resp_650 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_trans'8743'tri'8658'resp_650 :: (AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14
du_trans'8743'tri'8658'resp_650 AgdaAny -> AgdaAny -> T_Tri_136
v0
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
         ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'691'_498 ((AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0) AgdaAny
v1 AgdaAny
v3)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 ->
         ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'737'_582 ((AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_136
v0) AgdaAny
v1 AgdaAny
v3)
-- Relation.Binary.Consequences._.wlog
d_wlog_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 -> ()) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
d_wlog_682 :: 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__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_wlog_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 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wlog_682 AgdaAny -> AgdaAny -> T__'8846'__30
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
du_wlog_682 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny
du_wlog_682 :: (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_wlog_682 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
  = let v5 :: t
v5 = (AgdaAny -> AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v3 AgdaAny
v4 in
    AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
         MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v6 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v6
         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v6
           -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v4 AgdaAny
v3 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v4 AgdaAny
v3 AgdaAny
v6)
         T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Consequences._.dec⇒weaklyDec
d_dec'8658'weaklyDec_734 ::
  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.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> Maybe AgdaAny
d_dec'8658'weaklyDec_734 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
d_dec'8658'weaklyDec_734 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> Maybe AgdaAny
du_dec'8658'weaklyDec_734 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
du_dec'8658'weaklyDec_734 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> Maybe AgdaAny
du_dec'8658'weaklyDec_734 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> Maybe AgdaAny
du_dec'8658'weaklyDec_734 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v1 AgdaAny
v2
  = (T_Dec_32 -> Maybe AgdaAny) -> AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe T_Dec_32 -> Maybe AgdaAny
MAlonzo.Code.Data.Maybe.Base.du_decToMaybe_24 ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v1 AgdaAny
v2)
-- Relation.Binary.Consequences._.dec⇒recomputable
d_dec'8658'recomputable_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.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_dec'8658'recomputable_742 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_dec'8658'recomputable_742 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
  = (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_dec'8658'recomputable_742 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
du_dec'8658'recomputable_742 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_dec'8658'recomputable_742 :: (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_dec'8658'recomputable_742 AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Dec_32 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Dec_32 -> AgdaAny
MAlonzo.Code.Relation.Nullary.du_recompute_60 ((AgdaAny -> AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_32
v0 AgdaAny
v1 AgdaAny
v2)
-- Relation.Binary.Consequences._.map-NonEmpty
d_map'45'NonEmpty_766 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Relation.Binary.Definitions.T_NonEmpty_316 ->
  MAlonzo.Code.Relation.Binary.Definitions.T_NonEmpty_316
d_map'45'NonEmpty_766 :: T_Level_18
-> T_Level_18
-> 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_NonEmpty_316
-> T_NonEmpty_316
d_map'45'NonEmpty_766 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 T_NonEmpty_316
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_NonEmpty_316 -> T_NonEmpty_316
du_map'45'NonEmpty_766 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 T_NonEmpty_316
v9
du_map'45'NonEmpty_766 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Definitions.T_NonEmpty_316 ->
  MAlonzo.Code.Relation.Binary.Definitions.T_NonEmpty_316
du_map'45'NonEmpty_766 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_NonEmpty_316 -> T_NonEmpty_316
du_map'45'NonEmpty_766 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 T_NonEmpty_316
v1
  = (AgdaAny -> AgdaAny -> AgdaAny -> T_NonEmpty_316)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_NonEmpty_316
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny -> T_NonEmpty_316
MAlonzo.Code.Relation.Binary.Definitions.C_nonEmpty_336
      ((T_NonEmpty_316 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_NonEmpty_316 -> AgdaAny
MAlonzo.Code.Relation.Binary.Definitions.d_x_330 (T_NonEmpty_316 -> AgdaAny
forall a b. a -> b
coe T_NonEmpty_316
v1))
      ((T_NonEmpty_316 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_NonEmpty_316 -> AgdaAny
MAlonzo.Code.Relation.Binary.Definitions.d_y_332 (T_NonEmpty_316 -> AgdaAny
forall a b. a -> b
coe T_NonEmpty_316
v1))
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 (T_NonEmpty_316 -> AgdaAny
MAlonzo.Code.Relation.Binary.Definitions.d_x_330 (T_NonEmpty_316 -> T_NonEmpty_316
forall a b. a -> b
coe T_NonEmpty_316
v1))
         (T_NonEmpty_316 -> AgdaAny
MAlonzo.Code.Relation.Binary.Definitions.d_y_332 (T_NonEmpty_316 -> T_NonEmpty_316
forall a b. a -> b
coe T_NonEmpty_316
v1))
         (T_NonEmpty_316 -> AgdaAny
MAlonzo.Code.Relation.Binary.Definitions.d_proof_334 (T_NonEmpty_316 -> T_NonEmpty_316
forall a b. a -> b
coe T_NonEmpty_316
v1)))
-- Relation.Binary.Consequences._.flip-Connex
d_flip'45'Connex_788 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  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.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_flip'45'Connex_788 :: T_Level_18
-> T_Level_18
-> 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__'8846'__30)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_flip'45'Connex_788 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> AgdaAny -> T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10
  = (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_flip'45'Connex_788 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10
du_flip'45'Connex_788 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_flip'45'Connex_788 :: (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_flip'45'Connex_788 AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v1 AgdaAny
v2
  = (T__'8846'__30 -> T__'8846'__30) -> AgdaAny -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30 -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.du_swap_78 ((AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T__'8846'__30
v0 AgdaAny
v2 AgdaAny
v1)
-- Relation.Binary.Consequences.subst⟶respˡ
d_subst'10230'resp'737'_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 -> ()) ->
  ((AgdaAny -> ()) ->
   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_subst'10230'resp'737'_796 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subst'10230'resp'737'_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 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = ((AgdaAny -> AgdaAny -> T_Level_18)
 -> ((AgdaAny -> T_Level_18)
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'737'_38 AgdaAny -> AgdaAny -> T_Level_18
v5 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
-- Relation.Binary.Consequences.subst⟶respʳ
d_subst'10230'resp'691'_798 ::
  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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_subst'10230'resp'691'_798 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subst'10230'resp'691'_798 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 -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = ((AgdaAny -> AgdaAny -> T_Level_18)
 -> ((AgdaAny -> T_Level_18)
     -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subst'8658'resp'691'_48 AgdaAny -> AgdaAny -> T_Level_18
v5 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
-- Relation.Binary.Consequences.subst⟶resp₂
d_subst'10230'resp'8322'_800 ::
  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.Agda.Builtin.Sigma.T_Σ_14
d_subst'10230'resp'8322'_800 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
d_subst'10230'resp'8322'_800 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 -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
  = (((AgdaAny -> T_Level_18)
  -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14)
-> ((AgdaAny -> T_Level_18)
    -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
forall a b. a -> b
coe ((AgdaAny -> T_Level_18)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
du_subst'8658'resp'8322'_58 (AgdaAny -> T_Level_18)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6
-- Relation.Binary.Consequences.P-resp⟶¬P-resp
d_P'45'resp'10230''172'P'45'resp_802 ::
  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) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_P'45'resp'10230''172'P'45'resp_802 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
d_P'45'resp'10230''172'P'45'resp_802 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_'8869'_4)
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.total⟶refl
d_total'10230'refl_804 ::
  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.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_total'10230'refl_804 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_total'10230'refl_804 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_Σ_14
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
  = (T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_total'8658'refl_102 T_Σ_14
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11
-- Relation.Binary.Consequences.total+dec⟶dec
d_total'43'dec'10230'dec_806 ::
  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 -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30) ->
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_total'43'dec'10230'dec_806 :: 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 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_total'43'dec'10230'dec_806 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 -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9 AgdaAny
v10 AgdaAny
v11
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> T__'8846'__30)
 -> (AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny
 -> AgdaAny
 -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T__'8846'__30)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
du_total'8743'dec'8658'dec_154 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> T__'8846'__30
v8 AgdaAny -> AgdaAny -> T_Dec_32
v9 AgdaAny
v10 AgdaAny
v11
-- Relation.Binary.Consequences.trans∧irr⟶asym
d_trans'8743'irr'10230'asym_808 ::
  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) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_trans'8743'irr'10230'asym_808 :: 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)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_trans'8743'irr'10230'asym_808 = 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)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.irr∧antisym⟶asym
d_irr'8743'antisym'10230'asym_810 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_irr'8743'antisym'10230'asym_810 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_irr'8743'antisym'10230'asym_810 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.asym⟶antisym
d_asym'10230'antisym_812 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_asym'10230'antisym_812 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_asym'10230'antisym_812 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 -> T_'8869'_4
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10
  = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
du_asym'8658'antisym_288
-- Relation.Binary.Consequences.asym⟶irr
d_asym'10230'irr_814 ::
  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.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_asym'10230'irr_814 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_asym'10230'irr_814 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_'8869'_4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.tri⟶asym
d_tri'10230'asym_816 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_tri'10230'asym_816 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_tri'10230'asym_816 = 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.tri⟶irr
d_tri'10230'irr_818 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4
d_tri'10230'irr_818 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
d_tri'10230'irr_818 = 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_'8869'_4
forall a. a
erased
-- Relation.Binary.Consequences.tri⟶dec≈
d_tri'10230'dec'8776'_820 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_tri'10230'dec'8776'_820 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_tri'10230'dec'8776'_820 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_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
  = ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'8776'_426 AgdaAny -> AgdaAny -> T_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
-- Relation.Binary.Consequences.tri⟶dec<
d_tri'10230'dec'60'_822 ::
  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.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_tri'10230'dec'60'_822 :: 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_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
d_tri'10230'dec'60'_822 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_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
  = ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> T_Dec_32)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> T_Dec_32
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> T_Dec_32
du_tri'8658'dec'60'_462 AgdaAny -> AgdaAny -> T_Tri_136
v6 AgdaAny
v7 AgdaAny
v8
-- Relation.Binary.Consequences.trans∧tri⟶respʳ≈
d_trans'8743'tri'10230'resp'691''8776'_824 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans'8743'tri'10230'resp'691''8776'_824 :: 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 -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans'8743'tri'10230'resp'691''8776'_824 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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
                                           AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 AgdaAny
v13 AgdaAny
v14
  = ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'691'_498 AgdaAny -> AgdaAny -> T_Tri_136
v9 AgdaAny
v10 AgdaAny
v12
-- Relation.Binary.Consequences.trans∧tri⟶respˡ≈
d_trans'8743'tri'10230'resp'737''8776'_826 ::
  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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_trans'8743'tri'10230'resp'737''8776'_826 :: 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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_trans'8743'tri'10230'resp'737''8776'_826 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
v6 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7
                                           AgdaAny -> AgdaAny -> T_Tri_136
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 AgdaAny
v12 AgdaAny
v13
  = ((AgdaAny -> AgdaAny -> T_Tri_136)
 -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> AgdaAny -> AgdaAny -> AgdaAny
du_trans'8743'tri'8658'resp'737'_582 AgdaAny -> AgdaAny -> T_Tri_136
v8 AgdaAny
v9 AgdaAny
v11
-- Relation.Binary.Consequences.trans∧tri⟶resp≈
d_trans'8743'tri'10230'resp'8776'_828 ::
  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 -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_136) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_trans'8743'tri'10230'resp'8776'_828 :: 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 -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Tri_136)
-> T_Σ_14
d_trans'8743'tri'10230'resp'8776'_828 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 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny -> AgdaAny -> T_Tri_136
v9
  = ((AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14)
-> (AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Tri_136) -> T_Σ_14
du_trans'8743'tri'8658'resp_650 AgdaAny -> AgdaAny -> T_Tri_136
v9
-- Relation.Binary.Consequences.dec⟶weaklyDec
d_dec'10230'weaklyDec_830 ::
  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.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> Maybe AgdaAny
d_dec'10230'weaklyDec_830 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
d_dec'10230'weaklyDec_830 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
  = ((AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny -> AgdaAny -> Maybe AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> Maybe AgdaAny
du_dec'8658'weaklyDec_734 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
-- Relation.Binary.Consequences.dec⟶recomputable
d_dec'10230'recomputable_832 ::
  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.Nullary.T_Dec_32) ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_dec'10230'recomputable_832 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_dec'10230'recomputable_832 T_Level_18
v0 T_Level_18
v1 T_Level_18
v2 T_Level_18
v3 T_Level_18
v4 AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8
  = ((AgdaAny -> AgdaAny -> T_Dec_32)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Dec_32)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
du_dec'8658'recomputable_742 AgdaAny -> AgdaAny -> T_Dec_32
v6 AgdaAny
v7 AgdaAny
v8