{-# 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.Data.Tree.AVL.Key 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.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Equality
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality
import qualified MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.Tree.AVL.Key.Key⁺
d_Key'8314'_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 -> ()
d_Key'8314'_58 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
d_Key'8314'_58 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Key._._≈∙_
d__'8776''8729'__62 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__62 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._._<⁺_
d__'60''8314'__72 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__72 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._<_<_
d__'60'_'60'__80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__80 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Key.⊥⁺<[_]<⊤⁺
d_'8869''8314''60''91'_'93''60''8868''8314'_90 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_90 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_90 ~T_StrictTotalOrder_1036
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_90
du_'8869''8314''60''91'_'93''60''8868''8314'_90 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_90 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_90
  = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((AgdaAny -> T__'60''8314'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93'_26
         (T__'60''8331'__20 -> AgdaAny
forall a b. a -> b
coe
            T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'8869''8331''60''91'_'93'_24))
      (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe
         T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.C_'91'_'93''60''8868''8314'_30)
-- Data.Tree.AVL.Key.refl⁺
d_refl'8314'_94 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_94 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4
du_refl'8314'_94 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_94 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_94 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1
  = ((AgdaAny -> AgdaAny)
 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Equality.du_'8776''177''45'refl_98
      (let v2 :: t
v2
             = (T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638)
-> AgdaAny -> t
forall a b. a -> b
coe
                 T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638
MAlonzo.Code.Relation.Binary.Bundles.du_decStrictPartialOrder_1098
                 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v3 :: t
v3
                = (T_DecStrictPartialOrder_638 -> T_DecSetoid_84) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_DecStrictPartialOrder_638 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.du_decSetoid_728 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2) in
          (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
               ((T_IsDecEquivalence_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                  T_IsDecEquivalence_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
                  ((T_DecSetoid_84 -> T_IsDecEquivalence_44) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_DecSetoid_84 -> T_IsDecEquivalence_44
MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3))))))
      Maybe (Maybe AgdaAny)
v1
-- Data.Tree.AVL.Key.sym⁺
d_sym'8314'_100 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_sym'8314'_100 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_100 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_100 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5
du_sym'8314'_100 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_sym'8314'_100 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_100 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'8776''8729'__20
 -> T__'8776''8729'__20)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Equality.du_'8776''177''45'sym_100
      (let v3 :: t
v3
             = (T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638)
-> AgdaAny -> t
forall a b. a -> b
coe
                 T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638
MAlonzo.Code.Relation.Binary.Bundles.du_decStrictPartialOrder_1098
                 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) in
       AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (let v4 :: t
v4
                = (T_DecStrictPartialOrder_638 -> T_DecSetoid_84) -> AgdaAny -> t
forall a b. a -> b
coe
                    T_DecStrictPartialOrder_638 -> T_DecSetoid_84
MAlonzo.Code.Relation.Binary.Bundles.du_decSetoid_728 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: t
v5
                   = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> t
forall a b. a -> b
coe
                       T_DecSetoid_84 -> T_Setoid_44
MAlonzo.Code.Relation.Binary.Bundles.du_setoid_108 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4) in
             (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_Setoid_44 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
                     T_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v5))))))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2
-- Data.Tree.AVL.Key.trans⁺
d_trans'8314'_108 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_trans'8314'_108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_108 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_108 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
du_trans'8314'_108 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_trans'8314'_108 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'trans_162
      (T_IsStrictPartialOrder_290
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_306
         ((T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290)
-> AgdaAny -> T_IsStrictPartialOrder_290
forall a b. a -> b
coe
            T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
            ((T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
               (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3
-- Data.Tree.AVL.Key.irrefl⁺
d_irrefl'8314'_114 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_irrefl'8314'_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
d_irrefl'8314'_114 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
forall a. a
erased
-- Data.Tree.AVL.Key.strictPartialOrder
d_strictPartialOrder_118 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_strictPartialOrder_118 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictPartialOrder_556
d_strictPartialOrder_118 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
  = T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_118 T_StrictTotalOrder_1036
v3
du_strictPartialOrder_118 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
du_strictPartialOrder_118 :: T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_118 T_StrictTotalOrder_1036
v0
  = (T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556)
-> AgdaAny -> T_StrictPartialOrder_556
forall a b. a -> b
coe
      T_IsStrictPartialOrder_290 -> T_StrictPartialOrder_556
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_11097
      ((T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290)
-> T_IsStrictPartialOrder_290 -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_290 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictPartialOrder_334
         (T_IsStrictTotalOrder_534 -> T_IsStrictPartialOrder_290
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_542
            ((T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534)
-> AgdaAny -> T_IsStrictTotalOrder_534
forall a b. a -> b
coe
               T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
               (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0))))
-- Data.Tree.AVL.Key.strictTotalOrder
d_strictTotalOrder_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_strictTotalOrder_202 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictTotalOrder_1036
d_strictTotalOrder_202 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_202 T_StrictTotalOrder_1036
v3
du_strictTotalOrder_202 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
du_strictTotalOrder_202 :: T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_202 T_StrictTotalOrder_1036
v0
  = (T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036)
-> AgdaAny -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
      T_IsStrictTotalOrder_534 -> T_StrictTotalOrder_1036
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_21059
      ((T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534)
-> T_IsStrictTotalOrder_534 -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_534 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictTotalOrder_338
         (T_StrictTotalOrder_1036 -> T_IsStrictTotalOrder_534
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1058
            (T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)))