{-# 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 Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Agda.Primitive qualified
import MAlonzo.Code.Data.Irrelevant qualified
import MAlonzo.Code.Relation.Binary.Bundles qualified
import MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Equality qualified
import MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict qualified
import MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict qualified
import MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality qualified
import MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict qualified
import MAlonzo.Code.Relation.Binary.Structures qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- 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 :: AgdaAny
v2
             = (T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638)
-> AgdaAny -> AgdaAny
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 :: AgdaAny
v3
                = (T_DecStrictPartialOrder_638 -> T_DecSetoid_84)
-> AgdaAny -> AgdaAny
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
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
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 :: AgdaAny
v3
             = (T_StrictTotalOrder_1036 -> T_DecStrictPartialOrder_638)
-> AgdaAny -> AgdaAny
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 :: AgdaAny
v4
                = (T_DecStrictPartialOrder_638 -> T_DecSetoid_84)
-> AgdaAny -> AgdaAny
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
v3) in
          AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (let v5 :: AgdaAny
v5
                   = (T_DecSetoid_84 -> T_Setoid_44) -> AgdaAny -> AgdaAny
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
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
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)))