{-# 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.Construct.Closure.Reflexive.Properties 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive
import qualified MAlonzo.Code.Relation.Binary.Definitions
import qualified MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Binary.Construct.Closure.Reflexive.Properties._.=[]⇒
d_'61''91''93''8658'_44 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'61''91''93''8658'_44 :: 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 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
d_'61''91''93''8658'_44 ~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
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10
                        AgdaAny
v11 T_ReflClosure_30
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_'61''91''93''8658'_44 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
du_'61''91''93''8658'_44 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'61''91''93''8658'_44 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_'61''91''93''8658'_44 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6)
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._._~ᵒ_
d__'126''7506'__62 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d__'126''7506'__62 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'126''7506'__62 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.fromSum
d_fromSum_68 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_fromSum_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
-> T_ReflClosure_30
d_fromSum_68 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 T__'8846'__30
v6 = T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68 T__'8846'__30
v6
du_fromSum_68 ::
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_fromSum_68 :: T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68 T__'8846'__30
v0
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v0 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v1
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v1
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             AgdaAny
v1
      T__'8846'__30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.toSum
d_toSum_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_toSum_76 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T__'8846'__30
d_toSum_76 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 T_ReflClosure_30
v6 = T_ReflClosure_30 -> T__'8846'__30
du_toSum_76 T_ReflClosure_30
v6
du_toSum_76 ::
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_toSum_76 :: T_ReflClosure_30 -> T__'8846'__30
du_toSum_76 T_ReflClosure_30
v0
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v0 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (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
forall a. a
erased
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v3
        -> (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 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
      T_ReflClosure_30
_ -> T__'8846'__30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.⊎⇔Refl
d_'8846''8660'Refl_84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Function.Bundles.T_Equivalence_1714
d_'8846''8660'Refl_84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Equivalence_1714
d_'8846''8660'Refl_84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5
  = T_Equivalence_1714
du_'8846''8660'Refl_84
du_'8846''8660'Refl_84 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1714
du_'8846''8660'Refl_84 :: T_Equivalence_1714
du_'8846''8660'Refl_84
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714)
-> AgdaAny -> AgdaAny -> T_Equivalence_1714
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_1714
MAlonzo.Code.Function.Bundles.du_mk'8660'_2298 ((T__'8846'__30 -> T_ReflClosure_30) -> AgdaAny
forall a b. a -> b
coe T__'8846'__30 -> T_ReflClosure_30
du_fromSum_68)
      ((T_ReflClosure_30 -> T__'8846'__30) -> AgdaAny
forall a b. a -> b
coe T_ReflClosure_30 -> T__'8846'__30
du_toSum_76)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.sym
d_sym_86 ::
  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.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_sym_86 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
d_sym_86 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_ReflClosure_30
v7 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_sym_86 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T_ReflClosure_30
v7
du_sym_86 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_sym_86 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30
du_sym_86 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
             AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
             ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6)
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.trans
d_trans_94 ::
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_trans_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
d_trans_94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 T_ReflClosure_30
v8 T_ReflClosure_30
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v7 T_ReflClosure_30
v8 T_ReflClosure_30
v9
du_trans_94 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_trans_94 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T_ReflClosure_30
v4 T_ReflClosure_30
v5
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v4 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v5 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
                    T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v9
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    AgdaAny
v9
             T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v8
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v5 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    AgdaAny
v8
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v11
               -> (AgdaAny -> T_ReflClosure_30) -> AgdaAny -> T_ReflClosure_30
forall a b. a -> b
coe
                    AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                    ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v8 AgdaAny
v11)
             T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ReflClosure_30
_ -> T_ReflClosure_30
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.antisym
d_antisym_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  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.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny
d_antisym_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> AgdaAny
d_antisym_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny
v6 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v7 AgdaAny
v8 ~AgdaAny
v9 T_ReflClosure_30
v10 T_ReflClosure_30
v11
  = (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny -> AgdaAny
v6 AgdaAny
v8 T_ReflClosure_30
v10 T_ReflClosure_30
v11
du_antisym_114 ::
  (AgdaAny -> AgdaAny) ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny
du_antisym_114 :: (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_ReflClosure_30
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v2 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
             T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
               -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny
v0 AgdaAny
v1
             MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v9
               -> ((AgdaAny -> T_Irrelevant_20) -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> T_Irrelevant_20) -> AgdaAny
MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                    AgdaAny
forall a. a
erased
             T_ReflClosure_30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_ReflClosure_30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.total
d_total_140 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
d_total_140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny
-> AgdaAny
-> T__'8846'__30
d_total_140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Tri_158
v4 AgdaAny
v5 AgdaAny
v6 = (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140 AgdaAny -> AgdaAny -> T_Tri_158
v4 AgdaAny
v5 AgdaAny
v6
du_total_140 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30
du_total_140 :: (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140 AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2 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
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v4
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                ((AgdaAny -> T_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                   AgdaAny
v4)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v5
           -> (AgdaAny -> T__'8846'__30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T__'8846'__30
MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38
                (T_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe
                   T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36)
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v6
           -> (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_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                   AgdaAny
v6)
         T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.dec
d_dec_174 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (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_dec_174 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_dec_174 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7 = (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_174 AgdaAny -> AgdaAny -> T_Dec_20
v4 AgdaAny -> AgdaAny -> T_Dec_20
v5 AgdaAny
v6 AgdaAny
v7
du_dec_174 ::
  (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_dec_174 :: (AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
du_dec_174 AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3
  = (T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      T_Equivalence_1714 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.du_map_18
      (T_Equivalence_1714 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_1714
du_'8846''8660'Refl_84)
      ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'8846''45'dec__86
         ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v0 AgdaAny
v2 AgdaAny
v3) ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Dec_20
v1 AgdaAny
v2 AgdaAny
v3))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.decidable
d_decidable_184 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_decidable_184 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny
-> AgdaAny
-> T_Dec_20
d_decidable_184 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> T_Tri_158
v4 AgdaAny
v5 AgdaAny
v6
  = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> T_Dec_20
du_decidable_184 AgdaAny -> AgdaAny -> T_Tri_158
v4 AgdaAny
v5 AgdaAny
v6
du_decidable_184 ::
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_decidable_184 :: (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> T_Dec_20
du_decidable_184 AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2
  = let v3 :: t
v3 = (AgdaAny -> AgdaAny -> T_Tri_158) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Tri_158
v0 AgdaAny
v1 AgdaAny
v2 in
    AgdaAny -> T_Dec_20
forall a b. a -> b
coe
      (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v3 of
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v4
           -> (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
                   ((AgdaAny -> T_ReflClosure_30) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44
                      AgdaAny
v4))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v5
           -> (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_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe
                      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36))
         MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v6
           -> (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)
         T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._..extendedlambda0
d_'46'extendedlambda0_220 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Relation.Binary.Definitions.T_Tri_158) ->
  AgdaAny ->
  AgdaAny ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda0_220 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> (T__'8801'__12 -> T_Irrelevant_20)
-> AgdaAny
-> T_ReflClosure_30
-> T_Irrelevant_20
d_'46'extendedlambda0_220 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> T_Irrelevant_20)
-> (T__'8801'__12 -> T_Irrelevant_20)
-> AgdaAny
-> T_ReflClosure_30
-> T_Irrelevant_20
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.respˡ
d_resp'737'_226 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp'737'_226 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp'737'_226 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 AgdaAny
v11 T_ReflClosure_30
v12
du_resp'737'_226 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp'737'_226 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T_ReflClosure_30
v4
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v4 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> AgdaAny
v6)
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v7
        -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v7
      T_ReflClosure_30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.respʳ
d_resp'691'_234 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  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 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp'691'_234 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp'691'_234 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Level_18
v6 ~AgdaAny -> AgdaAny -> T_Level_18
v7 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234
du_resp'691'_234 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp'691'_234 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234 = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.resp
d_resp_250 ::
  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.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
d_resp_250 :: 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
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
d_resp_250 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T_ReflClosure_30
v9
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny
du_resp_250 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny
v7 AgdaAny
v8 T_ReflClosure_30
v9
du_resp_250 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30 ->
  AgdaAny -> AgdaAny
du_resp_250 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_ReflClosure_30 -> AgdaAny -> AgdaAny
du_resp_250 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 T_ReflClosure_30
v3
  = case T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe T_ReflClosure_30
v3 of
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
        -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v5 -> AgdaAny
v5)
      MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_'91'_'93'_44 AgdaAny
v6
        -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v6
      T_ReflClosure_30
_ -> AgdaAny -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.resp₂
d_resp'8322'_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_resp'8322'_270 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
d_resp'8322'_270 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> AgdaAny -> T_Level_18
v4 ~AgdaAny -> AgdaAny -> T_Level_18
v5 = T_Σ_14 -> T_Σ_14
du_resp'8322'_270
du_resp'8322'_270 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_resp'8322'_270 :: T_Σ_14 -> T_Σ_14
du_resp'8322'_270
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map_128 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'737'_226)
      ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> AgdaAny
-> AgdaAny
du_resp'691'_234))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._._~ᵒ_
d__'126''7506'__282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) -> AgdaAny -> AgdaAny -> ()
d__'126''7506'__282 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d__'126''7506'__282 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isPreorder
d_isPreorder_284 ::
  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.Structures.T_IsPreorder_70
d_isPreorder_284 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
d_isPreorder_284 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4
du_isPreorder_284 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
du_isPreorder_284 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0
  = (T_IsEquivalence_26
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> 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 -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> T_ReflClosure_30 -> AgdaAny
forall a b. a -> b
coe T_ReflClosure_30
du_'46'extendedlambda0_288)
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T_ReflClosure_30
 -> T_ReflClosure_30
 -> T_ReflClosure_30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_ReflClosure_30
-> T_ReflClosure_30
-> T_ReflClosure_30
du_trans_94 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._..extendedlambda0
d_'46'extendedlambda0_288 ::
  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.Equality.T__'8801'__12 ->
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
d_'46'extendedlambda0_288 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T_ReflClosure_30
d_'46'extendedlambda0_288 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v4 ~AgdaAny
v5 ~AgdaAny
v6 ~T__'8801'__12
v7
  = T_ReflClosure_30
du_'46'extendedlambda0_288
du_'46'extendedlambda0_288 ::
  MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.T_ReflClosure_30
du_'46'extendedlambda0_288 :: T_ReflClosure_30
du_'46'extendedlambda0_288
  = T_ReflClosure_30 -> T_ReflClosure_30
forall a b. a -> b
coe
      T_ReflClosure_30
MAlonzo.Code.Relation.Binary.Construct.Closure.Reflexive.C_refl_36
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isPartialOrder
d_isPartialOrder_290 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
d_isPartialOrder_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictPartialOrder_290
-> T_IsPartialOrder_174
d_isPartialOrder_290 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictPartialOrder_290
v4 = T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_isPartialOrder_290 T_IsStrictPartialOrder_290
v4
du_isPartialOrder_290 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictPartialOrder_290 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
du_isPartialOrder_290 :: T_IsStrictPartialOrder_290 -> T_IsPartialOrder_174
du_isPartialOrder_290 T_IsStrictPartialOrder_290
v0
  = (T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPartialOrder_174)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny -> 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
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_IsPreorder_70)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
du_isPreorder_284
         ((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)))
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> ((AgdaAny -> AgdaAny)
 -> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny)
-> AgdaAny -> T_ReflClosure_30 -> T_ReflClosure_30 -> AgdaAny
du_antisym_114 AgdaAny
forall a. a
erased AgdaAny
v1 AgdaAny
v3 AgdaAny
v4)
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isDecPartialOrder
d_isDecPartialOrder_326 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_336 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
d_isDecPartialOrder_326 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsDecStrictPartialOrder_336
-> T_IsDecPartialOrder_224
d_isDecPartialOrder_326 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsDecStrictPartialOrder_336
v4
  = T_IsDecStrictPartialOrder_336 -> T_IsDecPartialOrder_224
du_isDecPartialOrder_326 T_IsDecStrictPartialOrder_336
v4
du_isDecPartialOrder_326 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecStrictPartialOrder_336 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecPartialOrder_224
du_isDecPartialOrder_326 :: T_IsDecStrictPartialOrder_336 -> T_IsDecPartialOrder_224
du_isDecPartialOrder_326 T_IsDecStrictPartialOrder_336
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_isPartialOrder_290
         ((T_IsDecStrictPartialOrder_336 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_336 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_346
            (T_IsDecStrictPartialOrder_336 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_336
v0)))
      ((T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__348 (T_IsDecStrictPartialOrder_336 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_336
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_dec_174
         ((T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'8799'__348 (T_IsDecStrictPartialOrder_336 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_336
v0))
         ((T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsDecStrictPartialOrder_336 -> AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Relation.Binary.Structures.d__'60''63'__350 (T_IsDecStrictPartialOrder_336 -> AgdaAny
forall a b. a -> b
coe T_IsDecStrictPartialOrder_336
v0)))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isTotalOrder
d_isTotalOrder_374 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
d_isTotalOrder_374 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_534
-> T_IsTotalOrder_404
d_isTotalOrder_374 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictTotalOrder_534
v4 = T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404
du_isTotalOrder_374 T_IsStrictTotalOrder_534
v4
du_isTotalOrder_374 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsTotalOrder_404
du_isTotalOrder_374 :: T_IsStrictTotalOrder_534 -> T_IsTotalOrder_404
du_isTotalOrder_374 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_isPartialOrder_290
         ((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_Tri_158)
 -> AgdaAny -> AgdaAny -> T__'8846'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny -> T_Tri_158)
-> AgdaAny -> AgdaAny -> T__'8846'__30
du_total_140
         ((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)))
-- Relation.Binary.Construct.Closure.Reflexive.Properties._.isDecTotalOrder
d_isDecTotalOrder_428 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
d_isDecTotalOrder_428 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> AgdaAny -> T_Level_18)
-> T_IsStrictTotalOrder_534
-> T_IsDecTotalOrder_460
d_isDecTotalOrder_428 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> AgdaAny -> T_Level_18
v3 T_IsStrictTotalOrder_534
v4
  = T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
du_isDecTotalOrder_428 T_IsStrictTotalOrder_534
v4
du_isDecTotalOrder_428 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsStrictTotalOrder_534 ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsDecTotalOrder_460
du_isDecTotalOrder_428 :: T_IsStrictTotalOrder_534 -> T_IsDecTotalOrder_460
du_isDecTotalOrder_428 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_isTotalOrder_374 (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__'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_dec_174
         ((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)))