{-# 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'_60 ::
  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_1280 -> ()
d_Key'8314'_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
d_Key'8314'_60 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Key._._≈∙_
d__'8776''8729'__64 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__64 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._._<⁺_
d__'60''8314'__74 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__74 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._<_<_
d__'60'_'60'__82 ::
  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_1280 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__82 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__82 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> 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'_92 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_92 :: T_StrictTotalOrder_1280 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_92 ~T_StrictTotalOrder_1280
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_92
du_'8869''8314''60''91'_'93''60''8868''8314'_92 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_92 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_92
  = (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'_96 ::
  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_1280 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_96 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4 = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_96 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4
du_refl'8314'_96 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_96 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_96 T_StrictTotalOrder_1280
v0 Maybe (Maybe AgdaAny)
v1
  = ((AgdaAny -> AgdaAny)
 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> (AgdaAny -> 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
      (T_IsEquivalence_28 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_36
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
               ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                  (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))))
      Maybe (Maybe AgdaAny)
v1
-- Data.Tree.AVL.Key.sym⁺
d_sym'8314'_102 ::
  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_1280 ->
  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'_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_102 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5
du_sym'8314'_102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  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'_102 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_102 T_StrictTotalOrder_1280
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 -> AgdaAny -> AgdaAny -> 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
      (T_IsEquivalence_28 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_sym_38
         ((T_IsStrictPartialOrder_370 -> T_IsEquivalence_28)
-> AgdaAny -> T_IsEquivalence_28
forall a b. a -> b
coe
            T_IsStrictPartialOrder_370 -> T_IsEquivalence_28
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_382
            ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
               ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
                  (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2
-- Data.Tree.AVL.Key.trans⁺
d_trans'8314'_110 ::
  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_1280 ->
  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'_110 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_110 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
  = T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_110 T_StrictTotalOrder_1280
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
du_trans'8314'_110 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  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'_110 :: T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_110 T_StrictTotalOrder_1280
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_168
      (T_IsStrictPartialOrder_370
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_386
         ((T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370)
-> AgdaAny -> T_IsStrictPartialOrder_370
forall a b. a -> b
coe
            T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
               (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3
-- Data.Tree.AVL.Key.irrefl⁺
d_irrefl'8314'_116 ::
  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_1280 ->
  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'_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
d_irrefl'8314'_116 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Irrelevant_20
forall a. a
erased
-- Data.Tree.AVL.Key.strictPartialOrder
d_strictPartialOrder_120 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
d_strictPartialOrder_120 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictPartialOrder_760
d_strictPartialOrder_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3
  = T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760
du_strictPartialOrder_120 T_StrictTotalOrder_1280
v3
du_strictPartialOrder_120 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_760
du_strictPartialOrder_120 :: T_StrictTotalOrder_1280 -> T_StrictPartialOrder_760
du_strictPartialOrder_120 T_StrictTotalOrder_1280
v0
  = (T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760)
-> AgdaAny -> T_StrictPartialOrder_760
forall a b. a -> b
coe
      T_IsStrictPartialOrder_370 -> T_StrictPartialOrder_760
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_842
      ((T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370)
-> T_IsStrictPartialOrder_370 -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_370 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictPartialOrder_340
         (T_IsStrictTotalOrder_624 -> T_IsStrictPartialOrder_370
MAlonzo.Code.Relation.Binary.Structures.d_isStrictPartialOrder_632
            ((T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624)
-> AgdaAny -> T_IsStrictTotalOrder_624
forall a b. a -> b
coe
               T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
               (T_StrictTotalOrder_1280 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0))))
-- Data.Tree.AVL.Key.strictTotalOrder
d_strictTotalOrder_212 ::
  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_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
d_strictTotalOrder_212 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1280
-> T_StrictTotalOrder_1280
d_strictTotalOrder_212 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1280
v3 = T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_212 T_StrictTotalOrder_1280
v3
du_strictTotalOrder_212 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1280
du_strictTotalOrder_212 :: T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
du_strictTotalOrder_212 T_StrictTotalOrder_1280
v0
  = (T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280)
-> AgdaAny -> T_StrictTotalOrder_1280
forall a b. a -> b
coe
      T_IsStrictTotalOrder_624 -> T_StrictTotalOrder_1280
MAlonzo.Code.Relation.Binary.Bundles.C_constructor_1386
      ((T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624)
-> T_IsStrictTotalOrder_624 -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_624 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictTotalOrder_344
         (T_StrictTotalOrder_1280 -> T_IsStrictTotalOrder_624
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_1302
            (T_StrictTotalOrder_1280 -> T_StrictTotalOrder_1280
forall a b. a -> b
coe T_StrictTotalOrder_1280
v0)))