{-# 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.Empty
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'_52 ::
  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_864 -> ()
d_Key'8314'_52 :: T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
d_Key'8314'_52 = T_Level_18
-> T_Level_18 -> T_Level_18 -> T_StrictTotalOrder_864 -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Key._._≈∙_
d__'8776''8729'__56 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__56 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._._<⁺_
d__'60''8314'__66 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__66 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Key._<_<_
d__'60'_'60'__74 ::
  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_864 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__74 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> T_Level_18
d__'60'_'60'__74 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> 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'_84 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_84 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_84 ~T_StrictTotalOrder_864
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_84
du_'8869''8314''60''91'_'93''60''8868''8314'_84 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_84 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_84
  = (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'_88 ::
  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_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_88 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_88 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_88 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4
du_refl'8314'_88 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
du_refl'8314'_88 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_88 T_StrictTotalOrder_864
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_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> t
forall a b. a -> b
coe
                 T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.du_strictPartialOrder_916
                 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) in
       (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (T_IsEquivalence_26 -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_refl_34
            ((T_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
               T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
               ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v2)))))
      Maybe (Maybe AgdaAny)
v1
-- Data.Tree.AVL.Key.sym⁺
d_sym'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_864 ->
  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'_94 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
d_sym'8314'_94 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_94 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5
du_sym'8314'_94 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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'_94 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_94 T_StrictTotalOrder_864
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_864 -> T_StrictPartialOrder_472)
-> AgdaAny -> t
forall a b. a -> b
coe
                 T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.du_strictPartialOrder_916
                 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) 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_IsStrictPartialOrder_266 -> T_IsEquivalence_26)
-> AgdaAny -> T_IsEquivalence_26
forall a b. a -> b
coe
               T_IsStrictPartialOrder_266 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_278
               ((T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                  T_StrictPartialOrder_472 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictPartialOrder_494
                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v3)))))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2
-- Data.Tree.AVL.Key.trans⁺
d_trans'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_864 ->
  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'_102 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
d_trans'8314'_102 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
  = T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_102 T_StrictTotalOrder_864
v3 Maybe (Maybe AgdaAny)
v4 Maybe (Maybe AgdaAny)
v5 Maybe (Maybe AgdaAny)
v6
du_trans'8314'_102 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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'_102 :: T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
du_trans'8314'_102 T_StrictTotalOrder_864
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_IsStrictTotalOrder_502
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Relation.Binary.Structures.d_trans_514
         ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> T_IsStrictTotalOrder_502
forall a b. a -> b
coe
            T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))
      Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3
-- Data.Tree.AVL.Key.irrefl⁺
d_irrefl'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_864 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_irrefl'8314'_108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
d_irrefl'8314'_108 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_'8869'_4
forall a. a
erased
-- Data.Tree.AVL.Key.strictPartialOrder
d_strictPartialOrder_112 ::
  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_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
d_strictPartialOrder_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictPartialOrder_472
d_strictPartialOrder_112 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3
  = T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_112 T_StrictTotalOrder_864
v3
du_strictPartialOrder_112 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_472
du_strictPartialOrder_112 :: T_StrictTotalOrder_864 -> T_StrictPartialOrder_472
du_strictPartialOrder_112 T_StrictTotalOrder_864
v0
  = (T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472)
-> AgdaAny -> T_StrictPartialOrder_472
forall a b. a -> b
coe
      T_IsStrictPartialOrder_266 -> T_StrictPartialOrder_472
MAlonzo.Code.Relation.Binary.Bundles.C_StrictPartialOrder'46'constructor_8957
      ((T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictPartialOrder_266 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictPartialOrder_334
         ((T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_IsStrictTotalOrder_502 -> T_IsStrictPartialOrder_266
MAlonzo.Code.Relation.Binary.Structures.du_isStrictPartialOrder_540
            ((T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
               T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
               (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0))))
-- Data.Tree.AVL.Key.strictTotalOrder
d_strictTotalOrder_182 ::
  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_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
d_strictTotalOrder_182 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_864
-> T_StrictTotalOrder_864
d_strictTotalOrder_182 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_864
v3 = T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_182 T_StrictTotalOrder_864
v3
du_strictTotalOrder_182 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864
du_strictTotalOrder_182 :: T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
du_strictTotalOrder_182 T_StrictTotalOrder_864
v0
  = (T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864)
-> AgdaAny -> T_StrictTotalOrder_864
forall a b. a -> b
coe
      T_IsStrictTotalOrder_502 -> T_StrictTotalOrder_864
MAlonzo.Code.Relation.Binary.Bundles.C_StrictTotalOrder'46'constructor_16739
      ((T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502)
-> T_IsStrictTotalOrder_502 -> AgdaAny
forall a b. a -> b
coe
         T_IsStrictTotalOrder_502 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Construct.Add.Extrema.Strict.du_'60''177''45'isStrictTotalOrder_338
         (T_StrictTotalOrder_864 -> T_IsStrictTotalOrder_502
MAlonzo.Code.Relation.Binary.Bundles.d_isStrictTotalOrder_886
            (T_StrictTotalOrder_864 -> T_StrictTotalOrder_864
forall a b. a -> b
coe T_StrictTotalOrder_864
v0)))