{-# 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.Double 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.Primitive
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.Double._IsRelatedTo_
d__IsRelatedTo__62 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d__IsRelatedTo__62 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T__IsRelatedTo__62
  = C_nonstrict_70 AgdaAny | C_equals_74 AgdaAny
-- Relation.Binary.Reasoning.Base.Double.start
d_start_76 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
d_start_76 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
d_start_76 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__62
v9
  = T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_start_76 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 T__IsRelatedTo__62
v9
du_start_76 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_start_76 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_start_76 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 T__IsRelatedTo__62
v3
  = case T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v3 of
      C_nonstrict_70 AgdaAny
v4 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4
      C_equals_74 AgdaAny
v4
        -> (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
v1 AgdaAny
v2 AgdaAny
v4
      T__IsRelatedTo__62
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.≡-go
d_'8801''45'go_82 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62 -> T__IsRelatedTo__62
d_'8801''45'go_82 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8801''45'go_82 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9 ~T__'8801'__12
v10 T__IsRelatedTo__62
v11
  = T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8801''45'go_82 T__IsRelatedTo__62
v11
du_'8801''45'go_82 :: T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8801''45'go_82 :: T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8801''45'go_82 T__IsRelatedTo__62
v0 = T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0
-- Relation.Binary.Reasoning.Base.Double..extendedlambda0
d_'46'extendedlambda0_88 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda0_88 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda0_88 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                         ~T__'8801'__12
v10 AgdaAny
v11 ~T__'8801'__12
v12
  = AgdaAny -> AgdaAny
du_'46'extendedlambda0_88 AgdaAny
v11
du_'46'extendedlambda0_88 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_88 :: AgdaAny -> AgdaAny
du_'46'extendedlambda0_88 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Double..extendedlambda1
d_'46'extendedlambda1_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_'46'extendedlambda1_94 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
-> T__'8801'__12
-> AgdaAny
d_'46'extendedlambda1_94 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 ~AgdaAny
v9
                         ~T__'8801'__12
v10 AgdaAny
v11 ~T__'8801'__12
v12
  = AgdaAny -> AgdaAny
du_'46'extendedlambda1_94 AgdaAny
v11
du_'46'extendedlambda1_94 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_94 :: AgdaAny -> AgdaAny
du_'46'extendedlambda1_94 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Binary.Reasoning.Base.Double.≲-go
d_'8818''45'go_96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
d_'8818''45'go_96 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8818''45'go_96 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T__IsRelatedTo__62
v11
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8818''45'go_96 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T__IsRelatedTo__62
v11
du_'8818''45'go_96 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8818''45'go_96 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8818''45'go_96 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T__IsRelatedTo__62
v5
  = case T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v5 of
      C_nonstrict_70 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__62) -> AgdaAny -> T__IsRelatedTo__62
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__62
C_nonstrict_70
             ((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
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4
                AgdaAny
v6)
      C_equals_74 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__62) -> AgdaAny -> T__IsRelatedTo__62
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__62
C_nonstrict_70
             ((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
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v6 AgdaAny
v4)
      T__IsRelatedTo__62
_ -> T__IsRelatedTo__62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.≈-go
d_'8776''45'go_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
d_'8776''45'go_106 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_'8776''45'go_106 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T__IsRelatedTo__62
v11
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 T_IsPreorder_70
v6 AgdaAny
v7 AgdaAny
v8 AgdaAny
v9 AgdaAny
v10 T__IsRelatedTo__62
v11
du_'8776''45'go_106 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_'8776''45'go_106 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 T_IsPreorder_70
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 T__IsRelatedTo__62
v5
  = case T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v5 of
      C_nonstrict_70 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__62) -> AgdaAny -> T__IsRelatedTo__62
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__62
C_nonstrict_70
             ((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
v3 AgdaAny
v2 AgdaAny
v1
                ((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
v1 AgdaAny
v2 AgdaAny
v4)
                AgdaAny
v6)
      C_equals_74 AgdaAny
v6
        -> (AgdaAny -> T__IsRelatedTo__62) -> AgdaAny -> T__IsRelatedTo__62
forall a b. a -> b
coe
             AgdaAny -> T__IsRelatedTo__62
C_equals_74
             ((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
v1 AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 AgdaAny
v6)
      T__IsRelatedTo__62
_ -> T__IsRelatedTo__62
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.stop
d_stop_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__62
d_stop_116 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> T__IsRelatedTo__62
d_stop_116 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 AgdaAny
v7 = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__62
du_stop_116 T_IsPreorder_70
v6 AgdaAny
v7
du_stop_116 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__62
du_stop_116 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__62
du_stop_116 T_IsPreorder_70
v0 AgdaAny
v1
  = (AgdaAny -> T__IsRelatedTo__62) -> AgdaAny -> T__IsRelatedTo__62
forall a b. a -> b
coe
      AgdaAny -> T__IsRelatedTo__62
C_equals_74
      ((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.Double.IsEquality
d_IsEquality_122 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_IsEquality_122 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 p
a9 = ()
data T_IsEquality_122 = C_isEquality_130
-- Relation.Binary.Reasoning.Base.Double.IsEquality?
d_IsEquality'63'_138 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_IsEquality'63'_138 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T_Dec_20
d_IsEquality'63'_138 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__62
v9
  = T__IsRelatedTo__62 -> T_Dec_20
du_IsEquality'63'_138 T__IsRelatedTo__62
v9
du_IsEquality'63'_138 ::
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_IsEquality'63'_138 :: T__IsRelatedTo__62 -> T_Dec_20
du_IsEquality'63'_138 T__IsRelatedTo__62
v0
  = case T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0 of
      C_nonstrict_70 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_74 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_122 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_122
C_isEquality_130))
      T__IsRelatedTo__62
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Binary.Reasoning.Base.Double.extractEquality
d_extractEquality_148 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny
d_extractEquality_148 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T_IsEquality_122
-> AgdaAny
d_extractEquality_148 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8 T__IsRelatedTo__62
v9 T_IsEquality_122
v10
  = T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny
du_extractEquality_148 T__IsRelatedTo__62
v9 T_IsEquality_122
v10
du_extractEquality_148 ::
  T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny
du_extractEquality_148 :: T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny
du_extractEquality_148 T__IsRelatedTo__62
v0 T_IsEquality_122
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_122 -> AgdaAny
forall a b. a -> b
coe T_IsEquality_122
v1)
      (case T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0 of
         C_equals_74 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
         T__IsRelatedTo__62
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Relation.Binary.Reasoning.Base.Double.equalitySubRelation
d_equalitySubRelation_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
d_equalitySubRelation_152 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> T_SubRelation_60
d_equalitySubRelation_152 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6
  = T_SubRelation_60
du_equalitySubRelation_152
du_equalitySubRelation_152 ::
  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.T_SubRelation_60
du_equalitySubRelation_152 :: T_SubRelation_60
du_equalitySubRelation_152
  = ((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__62 -> T_Dec_20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__62 -> T_Dec_20
du_IsEquality'63'_138 AgdaAny
v2)
      (\ AgdaAny
v0 AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 -> (T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__IsRelatedTo__62 -> T_IsEquality_122 -> AgdaAny
du_extractEquality_148 AgdaAny
v2 AgdaAny
v3)
-- Relation.Binary.Reasoning.Base.Double._.begin_
d_begin__156 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
d_begin__156 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
d_begin__156 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 = T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_begin__156 T_IsPreorder_70
v6
du_begin__156 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_begin__156 :: T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_begin__156 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> 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 -> T__IsRelatedTo__62 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny
du_start_76 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Reasoning.Base.Double._.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 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> AgdaAny
d_begin__160 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> AgdaAny
d_begin__160 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 = AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> AgdaAny
du_begin__160
du_begin__160 ::
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> AgdaAny
du_begin__160 :: AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> AgdaAny
du_begin__160
  = let v0 :: b
v0 = T_SubRelation_60 -> b
forall a b. a -> b
coe T_SubRelation_60
du_equalitySubRelation_152 in
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> 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.Double._.step-≡
d_step'45''8801'_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
d_step'45''8801'_164 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801'_164 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801'_164
du_step'45''8801'_164 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
du_step'45''8801'_164 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801'_164
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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.Double._.step-≡-∣
d_step'45''8801''45''8739'_166 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> AgdaAny -> T__IsRelatedTo__62 -> T__IsRelatedTo__62
d_step'45''8801''45''8739'_166 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
d_step'45''8801''45''8739'_166 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6 ~AgdaAny
v7 ~AgdaAny
v8
                               T__IsRelatedTo__62
v9
  = T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_step'45''8801''45''8739'_166 T__IsRelatedTo__62
v9
du_step'45''8801''45''8739'_166 ::
  T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_step'45''8801''45''8739'_166 :: T__IsRelatedTo__62 -> T__IsRelatedTo__62
du_step'45''8801''45''8739'_166 T__IsRelatedTo__62
v0 = T__IsRelatedTo__62 -> T__IsRelatedTo__62
forall a b. a -> b
coe T__IsRelatedTo__62
v0
-- Relation.Binary.Reasoning.Base.Double._.step-≡-⟨
d_step'45''8801''45''10216'_168 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
d_step'45''8801''45''10216'_168 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''45''10216'_168 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''45''10216'_168
du_step'45''8801''45''10216'_168 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
du_step'45''8801''45''10216'_168 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''45''10216'_168
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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.Double._.step-≡-⟩
d_step'45''8801''45''10217'_170 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
d_step'45''8801''45''10217'_170 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''45''10217'_170 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''45''10217'_170
du_step'45''8801''45''10217'_170 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
du_step'45''8801''45''10217'_170 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''45''10217'_170
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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.Double._.step-≡˘
d_step'45''8801''728'_172 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
d_step'45''8801''728'_172 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
d_step'45''8801''728'_172 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 ~T_IsPreorder_70
v6
  = AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''728'_172
du_step'45''8801''728'_172 ::
  AgdaAny ->
  AgdaAny ->
  AgdaAny ->
  T__IsRelatedTo__62 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  T__IsRelatedTo__62
du_step'45''8801''728'_172 :: AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
du_step'45''8801''728'_172
  = ((AgdaAny
  -> AgdaAny -> AgdaAny -> T__'8801'__12 -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__'8801'__12
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__'8801'__12
-> T__IsRelatedTo__62
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.Double._.step-≈
d_step'45''8776'_176 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8776'_176 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8776'_176 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776'_176 T_IsPreorder_70
v6
du_step'45''8776'_176 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8776'_176 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776'_176 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Reasoning.Base.Double._.step-≈-⟨
d_step'45''8776''45''10216'_178 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8776''45''10216'_178 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8776''45''10216'_178 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''45''10216'_178 T_IsPreorder_70
v6
du_step'45''8776''45''10216'_178 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8776''45''10216'_178 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''45''10216'_178 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
      ((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.Double._.step-≈-⟩
d_step'45''8776''45''10217'_180 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8776''45''10217'_180 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8776''45''10217'_180 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''45''10217'_180 T_IsPreorder_70
v6
du_step'45''8776''45''10217'_180 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8776''45''10217'_180 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''45''10217'_180 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Reasoning.Base.Double._.step-≈˘
d_step'45''8776''728'_182 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8776''728'_182 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8776''728'_182 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''728'_182 T_IsPreorder_70
v6
du_step'45''8776''728'_182 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8776''728'_182 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8776''728'_182 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8776''45'go_106 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
      ((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.Double._.step-≲
d_step'45''8818'_186 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8818'_186 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8818'_186 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8818'_186 T_IsPreorder_70
v6
du_step'45''8818'_186 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8818'_186 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8818'_186 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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''8818'_304
      ((T_IsPreorder_70
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8818''45'go_96 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Reasoning.Base.Double._._∎
d__'8718'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__62
d__'8718'_190 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> T__IsRelatedTo__62
d__'8718'_190 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6 = T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__62
du__'8718'_190 T_IsPreorder_70
v6
du__'8718'_190 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny -> T__IsRelatedTo__62
du__'8718'_190 :: T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__62
du__'8718'_190 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__IsRelatedTo__62
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__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70 -> AgdaAny -> T__IsRelatedTo__62
du_stop_116 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))
-- Relation.Binary.Reasoning.Base.Double._.step-∼
d_step'45''8764'_194 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> ()) ->
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
d_step'45''8764'_194 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> ())
-> T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
d_step'45''8764'_194 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> AgdaAny -> ()
v4 ~AgdaAny -> AgdaAny -> ()
v5 T_IsPreorder_70
v6
  = T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8764'_194 T_IsPreorder_70
v6
du_step'45''8764'_194 ::
  MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
  AgdaAny ->
  AgdaAny ->
  AgdaAny -> T__IsRelatedTo__62 -> AgdaAny -> T__IsRelatedTo__62
du_step'45''8764'_194 :: T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
du_step'45''8764'_194 T_IsPreorder_70
v0
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> AgdaAny
-> T__IsRelatedTo__62
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''8764'_300
      ((T_IsPreorder_70
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny
 -> T__IsRelatedTo__62
 -> T__IsRelatedTo__62)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__IsRelatedTo__62
-> T__IsRelatedTo__62
du_'8818''45'go_96 (T_IsPreorder_70 -> AgdaAny
forall a b. a -> b
coe T_IsPreorder_70
v0))