{-# 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
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
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
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
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
~()
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
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)
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
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
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
~()
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
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)
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
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)))
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)))
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
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
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
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)
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
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
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
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
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
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
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)