{-# 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.Reasoning.Base.Triple 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.Relation.Binary.Reasoning.Syntax
import qualified MAlonzo.Code.Relation.Binary.Structures
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Relation.Binary.Reasoning.Base.Triple._IsRelatedTo_
d__IsRelatedTo__78 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d__IsRelatedTo__78 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 p
a12 p
a13
                   p
a14 p
a15 p
a16
  = ()
data T__IsRelatedTo__78
  = C_strict_86 AgdaAny | C_nonstrict_90 AgdaAny |
    C_equals_94 AgdaAny
-- Relation.Binary.Reasoning.Base.Triple.start
d_start_96 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny
d_start_96 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
d_start_96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
           ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__78
v17
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
du_start_96 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__78
v17
du_start_96 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny
du_start_96 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
du_start_96 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__78
v4
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v4 of
      C_strict_86 AgdaAny
v5 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5
      C_nonstrict_90 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
      C_equals_94 AgdaAny
v5
        -> (T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_IsPreorder_70 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 T_IsPreorder_70
v0 AgdaAny
v2 AgdaAny
v3 AgdaAny
v5
      T__IsRelatedTo__78
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.≡-go
d_'8801''45'go_104 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78 -> T__IsRelatedTo__78
d_'8801''45'go_104 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
d_'8801''45'go_104 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                   ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 ~AgdaAny
v17 ~T__'8801'__12
v18 T__IsRelatedTo__78
v19
  = T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'8801''45'go_104 T__IsRelatedTo__78
v19
du_'8801''45'go_104 :: T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'8801''45'go_104 :: T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'8801''45'go_104 T__IsRelatedTo__78
v0 = T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda0
d_'46'extendedlambda0_110 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_110 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_110 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9
                          ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 ~AgdaAny
v17 ~T__'8801'__12
v18 AgdaAny
v19 ~T__'8801'__12
v20
  = AgdaAny -> AgdaAny
du_'46'extendedlambda0_110 AgdaAny
v19
du_'46'extendedlambda0_110 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_110 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_110 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda1
d_'46'extendedlambda1_116 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_116 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_116 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9
                          ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 ~AgdaAny
v17 ~T__'8801'__12
v18 AgdaAny
v19 ~T__'8801'__12
v20
  = AgdaAny -> AgdaAny
du_'46'extendedlambda1_116 AgdaAny
v19
du_'46'extendedlambda1_116 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_116 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_116 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda2
d_'46'extendedlambda2_122 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda2_122 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda2_122 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9
                          ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 ~AgdaAny
v17 ~T__'8801'__12
v18 AgdaAny
v19 ~T__'8801'__12
v20
  = AgdaAny -> AgdaAny
du_'46'extendedlambda2_122 AgdaAny
v19
du_'46'extendedlambda2_122 :: AgdaAny -> AgdaAny
du_'46'extendedlambda2_122 :: AgdaAny -> AgdaAny
du_'46'extendedlambda2_122 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple.≈-go
d_'8776''45'go_124 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
d_'8776''45'go_124 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
d_'8776''45'go_124 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11
                   ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 T_IsPreorder_70
v8 T_Σ_14
v11 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
du_'8776''45'go_124 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'8776''45'go_124 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 T_IsPreorder_70
v0 T_Σ_14
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__IsRelatedTo__78
v6
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v6 of
      C_strict_86 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_strict_86
             ((T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30 T_Σ_14
v1 AgdaAny
v4 AgdaAny
v3 AgdaAny
v2
                ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                   (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                      (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
                   AgdaAny
v2 AgdaAny
v3 AgdaAny
v5)
                AgdaAny
v7)
      C_nonstrict_90 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_nonstrict_90
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'737''45''8776'_114
                T_IsPreorder_70
v0 AgdaAny
v4 AgdaAny
v3 AgdaAny
v2
                ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
                   (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                      (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
                   AgdaAny
v2 AgdaAny
v3 AgdaAny
v5)
                AgdaAny
v7)
      C_equals_94 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_equals_94
             ((T_IsEquivalence_26
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsEquivalence_26
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_38
                (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
                   (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
                AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7)
      T__IsRelatedTo__78
_ -> T__IsRelatedTo__78
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.≤-go
d_'8804''45'go_138 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
d_'8804''45'go_138 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
d_'8804''45'go_138 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11
                   ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8804''45'go_138 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
du_'8804''45'go_138 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'8804''45'go_138 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8804''45'go_138 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__IsRelatedTo__78
v6
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v6 of
      C_strict_86 AgdaAny
v7 -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__78
C_strict_86 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v7)
      C_nonstrict_90 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_nonstrict_90
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_84 T_IsPreorder_70
v0 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5
                AgdaAny
v7)
      C_equals_94 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_nonstrict_90
             ((T_IsPreorder_70
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_IsPreorder_70
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'691''45''8776'_116
                T_IsPreorder_70
v0 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v7 AgdaAny
v5)
      T__IsRelatedTo__78
_ -> T__IsRelatedTo__78
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.<-go
d_'60''45'go_152 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
d_'60''45'go_152 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
d_'60''45'go_152 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11
                 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'60''45'go_152 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 T__IsRelatedTo__78
v19
du_'60''45'go_152 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_'60''45'go_152 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'60''45'go_152 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 T__IsRelatedTo__78
v7
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v7 of
      C_strict_86 AgdaAny
v8 -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__78
C_strict_86 ((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
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
      C_nonstrict_90 AgdaAny
v8 -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__78
C_strict_86 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
      C_equals_94 AgdaAny
v8
        -> (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__78
C_strict_86
             ((T_Σ_14 -> AgdaAny)
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28 T_Σ_14
v1 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 AgdaAny
v8 AgdaAny
v6)
      T__IsRelatedTo__78
_ -> T__IsRelatedTo__78
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.stop
d_stop_166 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T__IsRelatedTo__78
d_stop_166 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T__IsRelatedTo__78
d_stop_166 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
           ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 AgdaAny
v15
  = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78
du_stop_166 T_IsPreorder_70
v8 AgdaAny
v15
du_stop_166 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__78
du_stop_166 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78
du_stop_166 T_IsPreorder_70
v0 AgdaAny
v1
  = (AgdaAny -> T__IsRelatedTo__78) -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
      AgdaAny -> T__IsRelatedTo__78
C_equals_94
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny)
-> T_IsEquivalence_26 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
         (T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> T_IsPreorder_70
forall a b. a -> b
coe T_IsPreorder_70
v0))
         AgdaAny
v1)
-- Relation.Binary.Reasoning.Base.Triple.IsStrict
d_IsStrict_172 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_IsStrict_172 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 p
a12 p
a13 p
a14
               p
a15 p
a16 p
a17
  = ()
data T_IsStrict_172 = C_isStrict_180
-- Relation.Binary.Reasoning.Base.Triple.IsStrict?
d_IsStrict'63'_188 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_IsStrict'63'_188 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T_Dec_20
d_IsStrict'63'_188 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                   ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__78
v17
  = T__IsRelatedTo__78 -> T_Dec_20
du_IsStrict'63'_188 T__IsRelatedTo__78
v17
du_IsStrict'63'_188 ::
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_IsStrict'63'_188 :: T__IsRelatedTo__78 -> T_Dec_20
du_IsStrict'63'_188 T__IsRelatedTo__78
v0
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0 of
      C_strict_86 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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_IsStrict_172 -> AgdaAny
forall a b. a -> b
coe T_IsStrict_172
C_isStrict_180))
      C_nonstrict_90 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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)
      C_equals_94 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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__IsRelatedTo__78
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.extractStrict
d_extractStrict_198 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny
d_extractStrict_198 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T_IsStrict_172
-> AgdaAny
d_extractStrict_198 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                    ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__78
v17 T_IsStrict_172
v18
  = T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny
du_extractStrict_198 T__IsRelatedTo__78
v17 T_IsStrict_172
v18
du_extractStrict_198 ::
  T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny
du_extractStrict_198 :: T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny
du_extractStrict_198 T__IsRelatedTo__78
v0 T_IsStrict_172
v1
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_IsStrict_172 -> AgdaAny
forall a b. a -> b
coe T_IsStrict_172
v1)
      (case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0 of
         C_strict_86 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__78
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Triple.strictRelation
d_strictRelation_202 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
d_strictRelation_202 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
d_strictRelation_202 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                     ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_SubRelation_60
du_strictRelation_202
du_strictRelation_202 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
du_strictRelation_202 :: T_SubRelation_60
du_strictRelation_202
  = ((AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_SubRelation_60)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.C_SubRelation'46'constructor_2989
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> (T__IsRelatedTo__78 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__78 -> T_Dec_20
du_IsStrict'63'_188 AgdaAny
v2)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__78 -> T_IsStrict_172 -> AgdaAny
du_extractStrict_198 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Reasoning.Base.Triple.IsEquality
d_IsEquality_208 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_IsEquality_208 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 p
a10 p
a11 p
a12 p
a13 p
a14
                 p
a15 p
a16 p
a17
  = ()
data T_IsEquality_208 = C_isEquality_216
-- Relation.Binary.Reasoning.Base.Triple.IsEquality?
d_IsEquality'63'_224 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_IsEquality'63'_224 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T_Dec_20
d_IsEquality'63'_224 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                     ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__78
v17
  = T__IsRelatedTo__78 -> T_Dec_20
du_IsEquality'63'_224 T__IsRelatedTo__78
v17
du_IsEquality'63'_224 ::
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_IsEquality'63'_224 :: T__IsRelatedTo__78 -> T_Dec_20
du_IsEquality'63'_224 T__IsRelatedTo__78
v0
  = case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0 of
      C_strict_86 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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)
      C_nonstrict_90 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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)
      C_equals_94 AgdaAny
v1
        -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
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_IsEquality_208 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_208
C_isEquality_216))
      T__IsRelatedTo__78
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.extractEquality
d_extractEquality_234 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny
d_extractEquality_234 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T_IsEquality_208
-> AgdaAny
d_extractEquality_234 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                      ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__78
v17 T_IsEquality_208
v18
  = T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny
du_extractEquality_234 T__IsRelatedTo__78
v17 T_IsEquality_208
v18
du_extractEquality_234 ::
  T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny
du_extractEquality_234 :: T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny
du_extractEquality_234 T__IsRelatedTo__78
v0 T_IsEquality_208
v1
  = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_IsEquality_208 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_208
v1)
      (case T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0 of
         C_equals_94 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__78
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Triple.eqRelation
d_eqRelation_238 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
d_eqRelation_238 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
d_eqRelation_238 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11
                 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_SubRelation_60
du_eqRelation_238
du_eqRelation_238 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
du_eqRelation_238 :: T_SubRelation_60
du_eqRelation_238
  = ((AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_SubRelation_60)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_SubRelation_60
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.C_SubRelation'46'constructor_2989
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 -> (T__IsRelatedTo__78 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__78 -> T_Dec_20
du_IsEquality'63'_224 AgdaAny
v2)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__78 -> T_IsEquality_208 -> AgdaAny
du_extractEquality_234 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Reasoning.Base.Triple._.begin_
d_begin__242 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny
d_begin__242 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
d_begin__242 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
             ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
du_begin__242 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
du_begin__242 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny
du_begin__242 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
du_begin__242 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
      ((T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
du_start_96 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1))
-- Relation.Binary.Reasoning.Base.Triple._.begin_
d_begin__246 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
d_begin__246 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> AgdaAny
d_begin__246 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
             ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__246
du_begin__246 ::
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__246 :: AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__246
  = let v0 :: b
v0 = T_SubRelation_60 -> b
forall a b. a -> b
coe T_SubRelation_60
du_eqRelation_238 in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v0) AgdaAny
v1 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Reasoning.Base.Triple._.begin_
d_begin__250 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
d_begin__250 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> AgdaAny
d_begin__250 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
             ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__250
du_begin__250 ::
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__250 :: AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
du_begin__250
  = let v0 :: b
v0 = T_SubRelation_60 -> b
forall a b. a -> b
coe T_SubRelation_60
du_strictRelation_202 in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      (\ AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 ->
         (T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
           T_SubRelation_60 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__126
           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v0) AgdaAny
v1 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Reasoning.Base.Triple._.begin-contradiction_
d_begin'45'contradiction__254 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
d_begin'45'contradiction__254 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> ()
-> ()
-> AgdaAny
d_begin'45'contradiction__254 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8
                              ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> () -> () -> AgdaAny
du_begin'45'contradiction__254
du_begin'45'contradiction__254 ::
  AgdaAny ->
  T__IsRelatedTo__78 ->
  AgdaAny -> MAlonzo.Code.Agda.Primitive.T_Level_18 -> () -> AgdaAny
du_begin'45'contradiction__254 :: AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> () -> () -> AgdaAny
du_begin'45'contradiction__254 AgdaAny
v0 T__IsRelatedTo__78
v1 AgdaAny
v2 ()
v3 ()
v4
  = AgdaAny -> AgdaAny
forall a b. a -> b
coe
      AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin'45'contradiction__246
-- Relation.Binary.Reasoning.Base.Triple._.step-≡
d_step'45''8801'_258 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
d_step'45''8801'_258 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
d_step'45''8801'_258 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                     ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801'_258
du_step'45''8801'_258 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
du_step'45''8801'_258 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801'_258
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801'_450
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Relation.Binary.Reasoning.Base.Triple._.step-≡-∣
d_step'45''8801''45''8739'_260 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__78 -> T__IsRelatedTo__78
d_step'45''8801''45''8739'_260 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
d_step'45''8801''45''8739'_260 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8
                               ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__78
v17
  = T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_step'45''8801''45''8739'_260 T__IsRelatedTo__78
v17
du_step'45''8801''45''8739'_260 ::
  T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_step'45''8801''45''8739'_260 :: T__IsRelatedTo__78 -> T__IsRelatedTo__78
du_step'45''8801''45''8739'_260 T__IsRelatedTo__78
v0 = T__IsRelatedTo__78 -> T__IsRelatedTo__78
forall a b. a -> b
coe T__IsRelatedTo__78
v0
-- Relation.Binary.Reasoning.Base.Triple._.step-≡-⟨
d_step'45''8801''45''10216'_262 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
d_step'45''8801''45''10216'_262 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
d_step'45''8801''45''10216'_262 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8
                                ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''45''10216'_262
du_step'45''8801''45''10216'_262 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
du_step'45''8801''45''10216'_262 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''45''10216'_262
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10216'_448
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Relation.Binary.Reasoning.Base.Triple._.step-≡-⟩
d_step'45''8801''45''10217'_264 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
d_step'45''8801''45''10217'_264 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
d_step'45''8801''45''10217'_264 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8
                                ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''45''10217'_264
du_step'45''8801''45''10217'_264 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
du_step'45''8801''45''10217'_264 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''45''10217'_264
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''45''10217'_436
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Relation.Binary.Reasoning.Base.Triple._.step-≡˘
d_step'45''8801''728'_266 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
d_step'45''8801''728'_266 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
d_step'45''8801''728'_266 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9
                          ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''728'_266
du_step'45''8801''728'_266 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__78 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__78
du_step'45''8801''728'_266 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
du_step'45''8801''728'_266
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__'8801'__12
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny
 -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8801''728'_452
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v4))
-- Relation.Binary.Reasoning.Base.Triple._.step-≈
d_step'45''8776'_270 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''8776'_270 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''8776'_270 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                     T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776'_270 T_IsPreorder_70
v8 T_Σ_14
v11
du_step'45''8776'_270 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''8776'_270 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776'_270 T_IsPreorder_70
v0 T_Σ_14
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776'_372
      ((T_IsPreorder_70
 -> T_Σ_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))
-- Relation.Binary.Reasoning.Base.Triple._.step-≈-⟨
d_step'45''8776''45''10216'_272 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''8776''45''10216'_272 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''8776''45''10216'_272 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8
                                ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''45''10216'_272 T_IsPreorder_70
v8 T_Σ_14
v11
du_step'45''8776''45''10216'_272 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''8776''45''10216'_272 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''45''10216'_272 T_IsPreorder_70
v0 T_Σ_14
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10216'_370
      ((T_IsPreorder_70
 -> T_Σ_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
-- Relation.Binary.Reasoning.Base.Triple._.step-≈-⟩
d_step'45''8776''45''10217'_274 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''8776''45''10217'_274 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''8776''45''10217'_274 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8
                                ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''45''10217'_274 T_IsPreorder_70
v8 T_Σ_14
v11
du_step'45''8776''45''10217'_274 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''8776''45''10217'_274 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''45''10217'_274 T_IsPreorder_70
v0 T_Σ_14
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''45''10217'_368
      ((T_IsPreorder_70
 -> T_Σ_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))
-- Relation.Binary.Reasoning.Base.Triple._.step-≈˘
d_step'45''8776''728'_276 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''8776''728'_276 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''8776''728'_276 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9
                          ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''728'_276 T_IsPreorder_70
v8 T_Σ_14
v11
du_step'45''8776''728'_276 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''8776''728'_276 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8776''728'_276 T_IsPreorder_70
v0 T_Σ_14
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8776''728'_374
      ((T_IsPreorder_70
 -> T_Σ_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8776''45'go_124 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))
      ((T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsEquivalence_26 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_36
         ((T_IsPreorder_70 -> T_IsEquivalence_26) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsPreorder_70 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
            (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0)))
-- Relation.Binary.Reasoning.Base.Triple._.step-≤
d_step'45''8804'_280 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''8804'_280 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''8804'_280 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10
                     ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8804'_280 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
du_step'45''8804'_280 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''8804'_280 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''8804'_280 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
      ((T_IsPreorder_70
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'8804''45'go_138 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1))
-- Relation.Binary.Reasoning.Base.Triple._.step-<
d_step'45''60'_284 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
d_step'45''60'_284 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
d_step'45''60'_284 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11
                   ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''60'_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Σ_14
v11 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13
du_step'45''60'_284 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__78 -> AgdaAny -> T__IsRelatedTo__78
du_step'45''60'_284 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
du_step'45''60'_284 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> AgdaAny
-> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''60'_312
      (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Σ_14
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__78
 -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__78
-> T__IsRelatedTo__78
du_'60''45'go_152 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2))
-- Relation.Binary.Reasoning.Base.Triple._._∎
d__'8718'_288 ::
  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.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny ->
   AgdaAny ->
   AgdaAny ->
   AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T__IsRelatedTo__78
d__'8718'_288 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T__IsRelatedTo__78
d__'8718'_288 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> T_Irrelevant_20
v9 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Σ_14
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
              ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v14
  = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78
du__'8718'_288 T_IsPreorder_70
v8
du__'8718'_288 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__78
du__'8718'_288 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78
du__'8718'_288 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__78
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
      ((T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__78
du_stop_166 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))