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

-- Relation.Binary.Reasoning.Base.Triple._IsRelatedTo_
d__IsRelatedTo__70 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d__IsRelatedTo__70 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
  = ()
data T__IsRelatedTo__70
  = C_strict_78 AgdaAny | C_nonstrict_82 AgdaAny |
    C_equals_86 AgdaAny
-- Relation.Binary.Reasoning.Base.Triple.IsStrict
d_IsStrict_92 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_IsStrict_92 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_IsStrict_92 = C_isStrict_100
-- Relation.Binary.Reasoning.Base.Triple.IsStrict?
d_IsStrict'63'_108 ::
  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 -> 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__70 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_IsStrict'63'_108 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T_Dec_32
d_IsStrict'63'_108 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                   ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16
  = T__IsRelatedTo__70 -> T_Dec_32
du_IsStrict'63'_108 T__IsRelatedTo__70
v16
du_IsStrict'63'_108 ::
  T__IsRelatedTo__70 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_IsStrict'63'_108 :: T__IsRelatedTo__70 -> T_Dec_32
du_IsStrict'63'_108 T__IsRelatedTo__70
v0
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0 of
      C_strict_78 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (T_IsStrict_92 -> AgdaAny
forall a b. a -> b
coe T_IsStrict_92
C_isStrict_100))
      C_nonstrict_82 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      C_equals_86 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      T__IsRelatedTo__70
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.extractStrict
d_extractStrict_118 ::
  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 -> 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__70 -> T_IsStrict_92 -> AgdaAny
d_extractStrict_118 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T_IsStrict_92
-> AgdaAny
d_extractStrict_118 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                    ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16 T_IsStrict_92
v17
  = T__IsRelatedTo__70 -> T_IsStrict_92 -> AgdaAny
du_extractStrict_118 T__IsRelatedTo__70
v16 T_IsStrict_92
v17
du_extractStrict_118 ::
  T__IsRelatedTo__70 -> T_IsStrict_92 -> AgdaAny
du_extractStrict_118 :: T__IsRelatedTo__70 -> T_IsStrict_92 -> AgdaAny
du_extractStrict_118 T__IsRelatedTo__70
v0 T_IsStrict_92
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_92 -> AgdaAny
forall a b. a -> b
coe T_IsStrict_92
v1)
      (case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0 of
         C_strict_78 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__70
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Triple.IsEquality
d_IsEquality_126 :: p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> p
-> ()
d_IsEquality_126 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_IsEquality_126 = C_isEquality_134
-- Relation.Binary.Reasoning.Base.Triple.IsEquality?
d_IsEquality'63'_142 ::
  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 -> 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__70 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_IsEquality'63'_142 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T_Dec_32
d_IsEquality'63'_142 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                     ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16
  = T__IsRelatedTo__70 -> T_Dec_32
du_IsEquality'63'_142 T__IsRelatedTo__70
v16
du_IsEquality'63'_142 ::
  T__IsRelatedTo__70 -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_IsEquality'63'_142 :: T__IsRelatedTo__70 -> T_Dec_32
du_IsEquality'63'_142 T__IsRelatedTo__70
v0
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0 of
      C_strict_78 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      C_nonstrict_82 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      C_equals_86 AgdaAny
v1
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
             ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22 (T_IsEquality_126 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_126
C_isEquality_134))
      T__IsRelatedTo__70
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.extractEquality
d_extractEquality_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 -> 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__70 -> T_IsEquality_126 -> AgdaAny
d_extractEquality_152 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T_IsEquality_126
-> AgdaAny
d_extractEquality_152 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                      ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16 T_IsEquality_126
v17
  = T__IsRelatedTo__70 -> T_IsEquality_126 -> AgdaAny
du_extractEquality_152 T__IsRelatedTo__70
v16 T_IsEquality_126
v17
du_extractEquality_152 ::
  T__IsRelatedTo__70 -> T_IsEquality_126 -> AgdaAny
du_extractEquality_152 :: T__IsRelatedTo__70 -> T_IsEquality_126 -> AgdaAny
du_extractEquality_152 T__IsRelatedTo__70
v0 T_IsEquality_126
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_126 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_126
v1)
      (case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0 of
         C_equals_86 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__70
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Triple.begin_
d_begin__160 ::
  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 -> 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__70 -> AgdaAny
d_begin__160 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
d_begin__160 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
             ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 T__IsRelatedTo__70
v16
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
du_begin__160 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v14 AgdaAny
v15 T__IsRelatedTo__70
v16
du_begin__160 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__70 -> AgdaAny
du_begin__160 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
du_begin__160 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 T__IsRelatedTo__70
v4
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v4 of
      C_strict_78 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_82 AgdaAny
v5 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5
      C_equals_86 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__70
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.begin-strict_
d_begin'45'strict__176 ::
  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 -> 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__70 -> AgdaAny -> AgdaAny
d_begin'45'strict__176 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> AgdaAny
d_begin'45'strict__176 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                       ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16 ~AgdaAny
v17
  = T__IsRelatedTo__70 -> AgdaAny
du_begin'45'strict__176 T__IsRelatedTo__70
v16
du_begin'45'strict__176 :: T__IsRelatedTo__70 -> AgdaAny
du_begin'45'strict__176 :: T__IsRelatedTo__70 -> AgdaAny
du_begin'45'strict__176 T__IsRelatedTo__70
v0
  = (T__IsRelatedTo__70 -> T_IsStrict_92 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__70 -> T_IsStrict_92 -> AgdaAny
du_extractStrict_118 (T__IsRelatedTo__70 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70
v0)
      ((T_Dec_32 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_32 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_36
         ((T__IsRelatedTo__70 -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70 -> T_Dec_32
du_IsStrict'63'_108 (T__IsRelatedTo__70 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70
v0)))
-- Relation.Binary.Reasoning.Base.Triple.begin-equality_
d_begin'45'equality__190 ::
  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 -> 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__70 -> AgdaAny -> AgdaAny
d_begin'45'equality__190 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> AgdaAny
d_begin'45'equality__190 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                         ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 T__IsRelatedTo__70
v16 ~AgdaAny
v17
  = T__IsRelatedTo__70 -> AgdaAny
du_begin'45'equality__190 T__IsRelatedTo__70
v16
du_begin'45'equality__190 :: T__IsRelatedTo__70 -> AgdaAny
du_begin'45'equality__190 :: T__IsRelatedTo__70 -> AgdaAny
du_begin'45'equality__190 T__IsRelatedTo__70
v0
  = (T__IsRelatedTo__70 -> T_IsEquality_126 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T__IsRelatedTo__70 -> T_IsEquality_126 -> AgdaAny
du_extractEquality_152 (T__IsRelatedTo__70 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70
v0)
      ((T_Dec_32 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Dec_32 -> AgdaAny
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_36
         ((T__IsRelatedTo__70 -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70 -> T_Dec_32
du_IsEquality'63'_142 (T__IsRelatedTo__70 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70
v0)))
-- Relation.Binary.Reasoning.Base.Triple.step-<
d_step'45''60'_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 -> 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__70 -> AgdaAny -> T__IsRelatedTo__70
d_step'45''60'_202 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> T__IsRelatedTo__70
d_step'45''60'_202 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11
                   AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''60'_202 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
du_step'45''60'_202 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__70 -> AgdaAny -> T__IsRelatedTo__70
du_step'45''60'_202 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Σ_14
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''60'_202 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 T_Σ_14
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v5 T__IsRelatedTo__70
v6 AgdaAny
v7
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v6 of
      C_strict_78 AgdaAny
v8 -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__70
C_strict_78 ((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
v7 AgdaAny
v8)
      C_nonstrict_82 AgdaAny
v8 -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__70
C_strict_78 ((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
v7 AgdaAny
v8)
      C_equals_86 AgdaAny
v8
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_strict_78
             ((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
v7)
      T__IsRelatedTo__70
_ -> T__IsRelatedTo__70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.step-≤
d_step'45''8804'_228 ::
  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 -> 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__70 -> AgdaAny -> T__IsRelatedTo__70
d_step'45''8804'_228 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> T__IsRelatedTo__70
d_step'45''8804'_228 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                     ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
  = T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8804'_228 T_IsPreorder_70
v8 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
du_step'45''8804'_228 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__70 -> AgdaAny -> T__IsRelatedTo__70
du_step'45''8804'_228 :: T_IsPreorder_70
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8804'_228 T_IsPreorder_70
v0 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T__IsRelatedTo__70
v5 AgdaAny
v6
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v5 of
      C_strict_78 AgdaAny
v7 -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe AgdaAny -> T__IsRelatedTo__70
C_strict_78 ((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
v6 AgdaAny
v7)
      C_nonstrict_82 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_nonstrict_82
             ((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
v6
                AgdaAny
v7)
      C_equals_86 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_nonstrict_82
             ((T_Σ_14 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_112
                   (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
                AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v7 AgdaAny
v6)
      T__IsRelatedTo__70
_ -> T__IsRelatedTo__70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.step-≈
d_step'45''8776'_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 -> 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__70 -> AgdaAny -> T__IsRelatedTo__70
d_step'45''8776'_254 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> T__IsRelatedTo__70
d_step'45''8776'_254 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 T_Σ_14
v10
                     ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8776'_254 T_IsPreorder_70
v8 T_Σ_14
v10 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
du_step'45''8776'_254 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__70 -> AgdaAny -> T__IsRelatedTo__70
du_step'45''8776'_254 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8776'_254 T_IsPreorder_70
v0 T_Σ_14
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T__IsRelatedTo__70
v5 AgdaAny
v6
  = case T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v5 of
      C_strict_78 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_strict_78
             ((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
v6)
                AgdaAny
v7)
      C_nonstrict_82 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_nonstrict_82
             ((T_Σ_14 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                ((T_IsPreorder_70 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_IsPreorder_70 -> T_Σ_14
MAlonzo.Code.Relation.Binary.Structures.du_'8764''45'resp'45''8776'_112
                   (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe 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
v6)
                AgdaAny
v7)
      C_equals_86 AgdaAny
v7
        -> (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__70
C_equals_86
             ((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
v6 AgdaAny
v7)
      T__IsRelatedTo__70
_ -> T__IsRelatedTo__70
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Triple.step-≈˘
d_step'45''8776''728'_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 -> 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__70 -> AgdaAny -> T__IsRelatedTo__70
d_step'45''8776''728'_280 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> AgdaAny
-> T__IsRelatedTo__70
d_step'45''8776''728'_280 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                          T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
  = T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8776''728'_280 T_IsPreorder_70
v8 T_Σ_14
v10 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 T__IsRelatedTo__70
v17 AgdaAny
v18
du_step'45''8776''728'_280 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__70 -> AgdaAny -> T__IsRelatedTo__70
du_step'45''8776''728'_280 :: T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8776''728'_280 T_IsPreorder_70
v0 T_Σ_14
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T__IsRelatedTo__70
v5 AgdaAny
v6
  = (T_IsPreorder_70
 -> T_Σ_14
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__70
 -> AgdaAny
 -> T__IsRelatedTo__70)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
forall a b. a -> b
coe
      T_IsPreorder_70
-> T_Σ_14
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__70
-> AgdaAny
-> T__IsRelatedTo__70
du_step'45''8776'_254 (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) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4)
      (T__IsRelatedTo__70 -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__70
v5)
      ((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
v3 AgdaAny
v2 AgdaAny
v6)
-- Relation.Binary.Reasoning.Base.Triple.step-≡
d_step'45''8801'_294 ::
  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 -> 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__70 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__70
d_step'45''8801'_294 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T__'8801'__12
-> T__IsRelatedTo__70
d_step'45''8801'_294 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10
                     ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__70
v17 ~T__'8801'__12
v18
  = T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801'_294 T__IsRelatedTo__70
v17
du_step'45''8801'_294 :: T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801'_294 :: T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801'_294 T__IsRelatedTo__70
v0 = T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda0
d_'46'extendedlambda0_302 ::
  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 -> 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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_302 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__'8801'__12
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_302 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                          ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 AgdaAny
v17 ~T__'8801'__12
v18 ~T__'8801'__12
v19
  = AgdaAny -> AgdaAny
du_'46'extendedlambda0_302 AgdaAny
v17
du_'46'extendedlambda0_302 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_302 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_302 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda1
d_'46'extendedlambda1_310 ::
  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 -> 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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_310 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__'8801'__12
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_310 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                          ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 AgdaAny
v17 ~T__'8801'__12
v18 ~T__'8801'__12
v19
  = AgdaAny -> AgdaAny
du_'46'extendedlambda1_310 AgdaAny
v17
du_'46'extendedlambda1_310 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_310 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_310 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple..extendedlambda2
d_'46'extendedlambda2_318 ::
  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 -> 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 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda2_318 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__'8801'__12
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda2_318 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                          ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 AgdaAny
v17 ~T__'8801'__12
v18 ~T__'8801'__12
v19
  = AgdaAny -> AgdaAny
du_'46'extendedlambda2_318 AgdaAny
v17
du_'46'extendedlambda2_318 :: AgdaAny -> AgdaAny
du_'46'extendedlambda2_318 :: AgdaAny -> AgdaAny
du_'46'extendedlambda2_318 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Triple.step-≡˘
d_step'45''8801''728'_326 ::
  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 -> 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__70 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__70
d_step'45''8801''728'_326 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
-> T__'8801'__12
-> T__IsRelatedTo__70
d_step'45''8801''728'_326 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 ~T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9
                          ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 ~AgdaAny
v14 ~AgdaAny
v15 ~AgdaAny
v16 T__IsRelatedTo__70
v17 ~T__'8801'__12
v18
  = T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801''728'_326 T__IsRelatedTo__70
v17
du_step'45''8801''728'_326 ::
  T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801''728'_326 :: T__IsRelatedTo__70 -> T__IsRelatedTo__70
du_step'45''8801''728'_326 T__IsRelatedTo__70
v0 = T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0
-- Relation.Binary.Reasoning.Base.Triple._≡⟨⟩_
d__'8801''10216''10217'__338 ::
  T__IsRelatedTo__70 -> T__IsRelatedTo__70
d__'8801''10216''10217'__338 :: T__IsRelatedTo__70 -> T__IsRelatedTo__70
d__'8801''10216''10217'__338 T__IsRelatedTo__70
v0 = T__IsRelatedTo__70 -> T__IsRelatedTo__70
forall a b. a -> b
coe T__IsRelatedTo__70
v0
-- Relation.Binary.Reasoning.Base.Triple._∎
d__'8718'_346 ::
  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 -> 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__70
d__'8718'_346 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> (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__70
d__'8718'_346 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~AgdaAny -> AgdaAny -> ()
v6 ~AgdaAny -> AgdaAny -> ()
v7 T_IsPreorder_70
v8 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v9 ~T_Σ_14
v10 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v12
              ~AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v13 AgdaAny
v14
  = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__70
du__'8718'_346 T_IsPreorder_70
v8 AgdaAny
v14
du__'8718'_346 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__70
du__'8718'_346 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__70
du__'8718'_346 T_IsPreorder_70
v0 AgdaAny
v1
  = (AgdaAny -> T__IsRelatedTo__70) -> AgdaAny -> T__IsRelatedTo__70
forall a b. a -> b
coe
      AgdaAny -> T__IsRelatedTo__70
C_equals_86
      ((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)