{-# 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.Indexed 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.DifferenceList
import qualified MAlonzo.Code.Data.Fin.Base
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Key
import qualified MAlonzo.Code.Data.Tree.AVL.Value
import qualified MAlonzo.Code.Function.Base
import qualified MAlonzo.Code.Relation.Binary.Bundles
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.Definitions
import qualified MAlonzo.Code.Relation.Binary.Structures

-- Data.Tree.AVL.Indexed._._<_<_
d__'60'_'60'__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_1036 ->
  Maybe (Maybe AgdaAny) -> AgdaAny -> Maybe (Maybe AgdaAny) -> ()
d__'60'_'60'__102 :: 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'__102 = 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.Indexed._._<⁺_
d__'60''8314'__104 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'60''8314'__104 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._._≈∙_
d__'8776''8729'__106 :: p -> p -> p -> p -> p -> p -> T_Level_18
d__'8776''8729'__106 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Key⁺
d_Key'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 -> ()
d_Key'8314'_108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
d_Key'8314'_108 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.irrefl⁺
d_irrefl'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_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'_110 :: 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'_110 = 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.Indexed._.refl⁺
d_refl'8314'_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_1036 ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Point.Equality.T__'8776''8729'__20
d_refl'8314'_112 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
d_refl'8314'_112 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_112 T_StrictTotalOrder_1036
v3
du_refl'8314'_112 ::
  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'_112 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
du_refl'8314'_112 T_StrictTotalOrder_1036
v0
  = (T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20)
-> AgdaAny -> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
forall a b. a -> b
coe T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny) -> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_refl'8314'_94 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
-- Data.Tree.AVL.Indexed._.strictPartialOrder
d_strictPartialOrder_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 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
d_strictPartialOrder_114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictPartialOrder_556
d_strictPartialOrder_114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3
  = T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_114 T_StrictTotalOrder_1036
v3
du_strictPartialOrder_114 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictPartialOrder_556
du_strictPartialOrder_114 :: T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
du_strictPartialOrder_114 T_StrictTotalOrder_1036
v0
  = (T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556)
-> AgdaAny -> T_StrictPartialOrder_556
forall a b. a -> b
coe
      T_StrictTotalOrder_1036 -> T_StrictPartialOrder_556
MAlonzo.Code.Data.Tree.AVL.Key.du_strictPartialOrder_118 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
-- Data.Tree.AVL.Indexed._.strictTotalOrder
d_strictTotalOrder_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_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
d_strictTotalOrder_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_StrictTotalOrder_1036
d_strictTotalOrder_116 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_116 T_StrictTotalOrder_1036
v3
du_strictTotalOrder_116 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036
du_strictTotalOrder_116 :: T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
du_strictTotalOrder_116 T_StrictTotalOrder_1036
v0
  = (T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036)
-> AgdaAny -> T_StrictTotalOrder_1036
forall a b. a -> b
coe
      T_StrictTotalOrder_1036 -> T_StrictTotalOrder_1036
MAlonzo.Code.Data.Tree.AVL.Key.du_strictTotalOrder_202 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
-- Data.Tree.AVL.Indexed._.sym⁺
d_sym'8314'_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 ->
  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'_118 :: 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'_118 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_118 T_StrictTotalOrder_1036
v3
du_sym'8314'_118 ::
  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'_118 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
du_sym'8314'_118 T_StrictTotalOrder_1036
v0
  = (T_StrictTotalOrder_1036
 -> 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 T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'8776''8729'__20
-> T__'8776''8729'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_sym'8314'_100 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
-- Data.Tree.AVL.Indexed._.trans⁺
d_trans'8314'_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_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'_120 :: 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'_120 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 = 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'_120 T_StrictTotalOrder_1036
v3
du_trans'8314'_120 ::
  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'_120 :: 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'_120 T_StrictTotalOrder_1036
v0
  = (T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> 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 T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
-- Data.Tree.AVL.Indexed._.⊥⁺<[_]<⊤⁺
d_'8869''8314''60''91'_'93''60''8868''8314'_122 ::
  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'_122 :: T_StrictTotalOrder_1036 -> AgdaAny -> T_Σ_14
d_'8869''8314''60''91'_'93''60''8868''8314'_122 ~T_StrictTotalOrder_1036
v0 ~AgdaAny
v1
  = T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122
du_'8869''8314''60''91'_'93''60''8868''8314'_122 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122 :: T_Σ_14
du_'8869''8314''60''91'_'93''60''8868''8314'_122
  = (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.Indexed._.Extrema.[_]-injective
d_'91'_'93''45'injective_138 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'91'_'93''45'injective_138 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
d_'91'_'93''45'injective_138 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> AgdaAny
-> AgdaAny
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.K&_
d_K'38'__144 :: p -> p -> p -> p -> p -> p -> T_Level_18
d_K'38'__144 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed._.Value
d_Value_148 :: p -> p -> p -> p -> p -> T_Level_18
d_Value_148 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed._.const
d_const_150 ::
  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.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_150 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
d_const_150 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 = T_Level_18 -> T_Level_18 -> T_Value_38
du_const_150
du_const_150 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_150 :: T_Level_18 -> T_Level_18 -> T_Value_38
du_const_150 T_Level_18
v0 T_Level_18
v1
  = T_Value_38 -> T_Value_38
forall a b. a -> b
coe T_Value_38
MAlonzo.Code.Data.Tree.AVL.Value.du_const_94
-- Data.Tree.AVL.Indexed._.fromPair
d_fromPair_152 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
d_fromPair_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 = T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_152
du_fromPair_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56
du_fromPair_152 :: T_Level_18 -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_152 T_Level_18
v0 T_Value_38
v1 T_Σ_14
v2
  = (T_Σ_14 -> T_K'38'__56) -> T_Σ_14 -> T_K'38'__56
forall a b. a -> b
coe T_Σ_14 -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.du_fromPair_86 T_Σ_14
v2
-- Data.Tree.AVL.Indexed._.key
d_key_154 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_154 :: T_K'38'__56 -> AgdaAny
d_key_154 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.toPair
d_toPair_156 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_156 :: T_K'38'__56 -> T_Σ_14
d_toPair_156 T_K'38'__56
v0
  = (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
      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0))
      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0))
-- Data.Tree.AVL.Indexed._.value
d_value_158 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_158 :: T_K'38'__56 -> AgdaAny
d_value_158 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.K&_.key
d_key_162 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_162 :: T_K'38'__56 -> AgdaAny
d_key_162 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.K&_.value
d_value_164 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_164 :: T_K'38'__56 -> AgdaAny
d_value_164 T_K'38'__56
v0
  = (T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_value_68 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v0)
-- Data.Tree.AVL.Indexed._.Value.family
d_family_168 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_168 :: T_Value_38 -> AgdaAny -> T_Level_18
d_family_168 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Value.respects
d_respects_170 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_170 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_170 T_Value_38
v0
  = (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
-- Data.Tree.AVL.Indexed.Tree
d_Tree_180 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> T_Level_18
d_Tree_180 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
data T_Tree_180
  = C_leaf_192 MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 |
    C_node_208 Integer Integer
               MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 T_Tree_180 T_Tree_180
               MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30
-- Data.Tree.AVL.Indexed._.ordered
d_ordered_224 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_180 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
d_ordered_224 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T__'60''8314'__20
d_ordered_224 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 T_Tree_180
v9
du_ordered_224 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_180 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20
du_ordered_224 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 T_Tree_180
v3
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v3 of
      C_leaf_192 T__'60''8314'__20
v4 -> T__'60''8314'__20 -> T__'60''8314'__20
forall a b. a -> b
coe T__'60''8314'__20
v4
      C_node_208 Integer
v4 Integer
v5 T_K'38'__56
v7 T_Tree_180
v8 T_Tree_180
v9 T__'8764'_'8852'__30
v10
        -> (T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T__'60''8314'__20
forall a b. a -> b
coe
             T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1
             ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
             Maybe (Maybe AgdaAny)
v2
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
                (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8))
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
du_ordered_224 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v7))))
                (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v9))
      T_Tree_180
_ -> T__'60''8314'__20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.Val
d_Val_236 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_236 :: T_Value_38 -> AgdaAny -> T_Level_18
d_Val_236 = T_Value_38 -> AgdaAny -> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.V≈
d_V'8776'_238 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_238 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_V'8776'_238 T_Value_38
v0
  = (T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v0)
-- Data.Tree.AVL.Indexed._.leaf-injective
d_leaf'45'injective_248 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  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.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_leaf'45'injective_248 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
d_leaf'45'injective_248 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.node-injective-key
d_node'45'injective'45'key_280 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Integer ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_180 ->
  T_Tree_180 ->
  T_Tree_180 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_node'45'injective'45'key_280 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
d_node'45'injective'45'key_280 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Integer
-> Integer
-> Integer
-> Integer
-> Integer
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_K'38'__56
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T__'8764'_'8852'__30
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.Tree.AVL.Indexed._.castˡ
d_cast'737'_290 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_180 -> T_Tree_180
d_cast'737'_290 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
d_cast'737'_290 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T__'60''8314'__20
v10 T_Tree_180
v11
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T__'60''8314'__20
v10 T_Tree_180
v11
du_cast'737'_290 ::
  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 ->
  T_Tree_180 -> T_Tree_180
du_cast'737'_290 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4 T_Tree_180
v5
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v5 of
      C_leaf_192 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> T_Tree_180
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_180
C_leaf_192
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v4
                T__'60''8314'__20
v6)
      C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T_Tree_180
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
-> T_Tree_180
du_cast'737'_290 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10))
             T_Tree_180
v11 T__'8764'_'8852'__30
v12
      T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.castʳ
d_cast'691'_316 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_180 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_180
d_cast'691'_316 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
d_cast'691'_316 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 ~Integer
v9 T_Tree_180
v10 T__'60''8314'__20
v11
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 T_Tree_180
v10 T__'60''8314'__20
v11
du_cast'691'_316 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  T_Tree_180 ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_180
du_cast'691'_316 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T_Tree_180
v4 T__'60''8314'__20
v5
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v4 of
      C_leaf_192 T__'60''8314'__20
v6
        -> (T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> T_Tree_180
forall a b. a -> b
coe
             T__'60''8314'__20 -> T_Tree_180
C_leaf_192
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T__'60''8314'__20
 -> T__'60''8314'__20)
-> T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T__'60''8314'__20
-> T__'60''8314'__20
MAlonzo.Code.Data.Tree.AVL.Key.du_trans'8314'_108 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 T__'60''8314'__20
v6
                T__'60''8314'__20
v5)
      C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10
             ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                   ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                      ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9))))
                (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v5))
             T__'8764'_'8852'__30
v12
      T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinˡ⁺
d_join'737''8314'_366 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8314'_366 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8314'_366 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join'737''8314'_366 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8314'_366 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_180
v4 T__'8764'_'8852'__30
v5
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
        -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
               -> (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
                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                    ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                       (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                       Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
               -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
                    (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4
                                 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 Integer
v0 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4
                                 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                         -> case AgdaAny -> T_Tree_180
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_208 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v16 T__'8764'_'8852'__30
v17
                                -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                       -> case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v16 of
                                            C_node_208 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_180
v23 T_Tree_180
v24 T__'8764'_'8852'__30
v25
                                              -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1 Integer
v19 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v23
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v20 Integer
v1 T_K'38'__56
v2 T_Tree_180
v24 T_Tree_180
v4
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                         T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                            T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_180
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                                  Integer
v1 T_K'38'__56
v2 T_Tree_180
v16 T_Tree_180
v4
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                  T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1)) T_K'38'__56
v14 T_Tree_180
v15
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1 Integer
v1 T_K'38'__56
v2 T_Tree_180
v16 T_Tree_180
v4
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                     T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinʳ⁺
d_join'691''8314'_456 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8314'_456 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8314'_456 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8314'_456 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8314'_456 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_180
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
        -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
             T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
               -> (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
                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                    ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                       Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                       (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                          (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                       T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
             MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
               -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
                    (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                         -> case AgdaAny -> T_Tree_180
forall a b. a -> b
coe AgdaAny
v7 of
                              C_node_208 Integer
v11 Integer
v12 T_K'38'__56
v14 T_Tree_180
v15 T_Tree_180
v16 T__'8764'_'8852'__30
v17
                                -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v17 of
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0 Integer
v0 T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v15
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                               T_Tree_180
v16
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                       -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                            ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                               T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                               (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
2 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                               (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v14
                                               ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                                                  (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v15
                                                  (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                                               T_Tree_180
v16
                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                  T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                                     T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                       -> case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v15 of
                                            C_node_208 Integer
v19 Integer
v20 T_K'38'__56
v22 T_Tree_180
v23 T_Tree_180
v24 T__'8764'_'8852'__30
v25
                                              -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                      Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                                      (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v0)) T_K'38'__56
v22
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0 Integer
v19 T_K'38'__56
v2 T_Tree_180
v3 T_Tree_180
v23
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_max'8764'_50
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v20 Integer
v0 T_K'38'__56
v14 T_Tree_180
v24 T_Tree_180
v16
                                                         ((T__'8764'_'8852'__30 -> T__'8764'_'8852'__30)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.du_'8764'max_58
                                                            (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v25)))
                                                      (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe
                                                         T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                                            T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                 T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                       T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                         -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer -> Integer -> Integer
addInt (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                 T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                       T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
             T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.joinˡ⁻
d_join'737''8315'_532 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'737''8315'_532 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'737''8315'_532 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Σ_14
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join'737''8315'_532 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'737''8315'_532 :: Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Σ_14
v3 T_Tree_180
v4 T__'8764'_'8852'__30
v5
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                      -> (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
                           ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                           ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                              (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
                      -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 Integer
v1 T_K'38'__56
v2 AgdaAny
v7 T_Tree_180
v4 T__'8764'_'8852'__30
v5))
                    T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v3 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
                  -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                         -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456
                                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0))
                                     (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                        ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                        (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v4))
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34)
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v0 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                        Integer
v6 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                              T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v10
                         -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v10)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                 ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> AgdaAny
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208
                                    (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                          T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v0))
                                    Integer
v1 T_K'38'__56
v2 AgdaAny
v8 T_Tree_180
v4 T__'8764'_'8852'__30
v5))
                       T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL.Indexed._.joinʳ⁻
d_join'691''8315'_594 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join'691''8315'_594 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join'691''8315'_594 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 Integer
v9 ~Integer
v10
                      T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
  = Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 Integer
v8 Integer
v9 T_K'38'__56
v11 T_Tree_180
v12 T_Σ_14
v13 T__'8764'_'8852'__30
v14
du_join'691''8315'_594 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join'691''8315'_594 :: Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 Integer
v0 Integer
v1 T_K'38'__56
v2 T_Tree_180
v3 T_Σ_14
v4 T__'8764'_'8852'__30
v5
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v1 of
      Integer
0 -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
               -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v6 of
                    T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                      -> (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
                           ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                              (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                           ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                              Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                              (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                 (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                              T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5)
                    MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v9
                      -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v9)
                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                              ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                 (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                              ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                 Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                                 (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                    ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                       T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                    (Integer -> Integer
forall a b. a -> b
coe (Integer
0 :: Integer)))
                                 T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v7 T__'8764'_'8852'__30
v5))
                    T_Fin_10
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      Integer
_ -> let v6 :: Integer
v6 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v1) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
                  -> case AgdaAny -> T_Fin_10
forall a b. a -> b
coe AgdaAny
v7 of
                       T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12
                         -> case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v5 of
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v1
                                        (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                           (T_Fin_10 -> T_Fin_10
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                        T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42))
                              T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1)
                                     ((T_Fin_10 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                        (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v1))
                                     (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v2)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                        ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                           (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                        (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v3))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8)
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42)
                              T__'8764'_'8852'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                       MAlonzo.Code.Data.Fin.Base.C_suc_16 T_Fin_10
v10
                         -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
v10)
                              ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                    (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                 ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> AgdaAny
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v0
                                    (T_Fin_10 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                                       ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> T_Fin_10
forall a b. a -> b
coe
                                          T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                                          (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
                                       (Integer -> Integer
forall a b. a -> b
coe Integer
v1))
                                    T_K'38'__56
v2 T_Tree_180
v3 AgdaAny
v8 T__'8764'_'8852'__30
v5))
                       T_Fin_10
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL.Indexed._.headTail
d_headTail_648 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_648 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Σ_14
d_headTail_648 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_180
v9
  = Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 Integer
v8 T_Tree_180
v9
du_headTail_648 ::
  Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_648 :: Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 Integer
v0 T_Tree_180
v1
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
      C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: b
v9
                 = let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> b
forall a b. a -> b
coe
                     (let v10 :: t
v10 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                               (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v6 of
                C_leaf_192 T__'60''8314'__20
v10
                  -> let v11 :: b
v11
                           = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2 of
                               AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                   let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v2) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                   AgdaAny -> b
forall a b. a -> b
coe
                                     (let v12 :: t
v12 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
                                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                               Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
                                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                               AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''43'_34
                            -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
                                 AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                     case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
                                       AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                           (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                             ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                                ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                                   (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)))
                                       AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                            -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                 ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                    ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)))
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
                T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
      T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.initLast
d_initLast_698 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_698 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Σ_14
d_initLast_698 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 Integer
v8 T_Tree_180
v9
  = Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 Integer
v8 T_Tree_180
v9
du_initLast_698 ::
  Integer -> T_Tree_180 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_698 :: Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 Integer
v0 T_Tree_180
v1
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
      C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
        -> let v9 :: b
v9
                 = let v9 :: Integer
v9 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                   AgdaAny -> b
forall a b. a -> b
coe
                     (let v10 :: t
v10 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v10 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v12 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                               (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v7 of
                C_leaf_192 T__'60''8314'__20
v10
                  -> let v11 :: b
v11
                           = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3 of
                               AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                   let v11 :: Integer
v11 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                                   AgdaAny -> b
forall a b. a -> b
coe
                                     (let v12 :: t
v12 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_initLast_698 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) in
                                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v12 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v13 AgdaAny
v14
                                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v14 of
                                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                                                    -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                                         ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                            (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                                            ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                               Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
                                                               (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)
                                                               (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v8)))
                                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                               AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v9 in
                     AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v8 of
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                            -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                 ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                    AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                    ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                       (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
                          T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                            -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0 of
                                 AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v0) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                                     (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                       AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v5)
                                       ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                          AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v10)
                                          ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                             (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
                                 AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11
                          T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11)
                T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v9)
      T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.join
d_join_754 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_180 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_join_754 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
d_join_754 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_180
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Maybe (Maybe AgdaAny)
v8 Integer
v9 Integer
v10 Integer
v11 T_Tree_180
v12 T_Tree_180
v13 T__'8764'_'8852'__30
v14
du_join_754 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  Integer ->
  Integer ->
  T_Tree_180 ->
  T_Tree_180 ->
  MAlonzo.Code.Data.Tree.AVL.Height.T__'8764'_'8852'__30 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_join_754 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Maybe (Maybe AgdaAny)
v3 Integer
v4 Integer
v5 Integer
v6 T_Tree_180
v7 T_Tree_180
v8 T__'8764'_'8852'__30
v9
  = let v10 :: b
v10
          = let v10 :: Integer
v10 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
            AgdaAny -> b
forall a b. a -> b
coe
              (let v11 :: t
v11 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v10) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8) in
               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v11 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v13 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                             -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12)
                                  ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                                     ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                           ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))))
                                     (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))
                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v8 of
         C_leaf_192 T__'60''8314'__20
v11
           -> let v12 :: b
v12
                    = case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5 of
                        AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                            let v12 :: Integer
v12 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v5) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
                            AgdaAny -> b
forall a b. a -> b
coe
                              (let v13 :: t
v13 = (Integer -> T_Tree_180 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_180 -> T_Σ_14
du_headTail_648 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8) in
                               AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v13 of
                                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v15 of
                                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v16 AgdaAny
v17
                                             -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                  Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                                  ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                     T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2)
                                                     ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                        AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                           ((T_K'38'__56 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                              T_K'38'__56 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_key_66
                                                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))))
                                                     (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16))
                                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v9)
                                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
                        AgdaAny
_ -> AgdaAny -> b
forall a b. a -> b
coe AgdaAny
forall a. a
v10 in
              AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (case T__'8764'_'8852'__30 -> T__'8764'_'8852'__30
forall a b. a -> b
coe T__'8764'_'8852'__30
v9 of
                   T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38
                     -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                          (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                          ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                             T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
                             (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
                   T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764''45'_42
                     -> case Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6 of
                          AgdaAny
_ | (Integer -> Integer -> Bool) -> AgdaAny -> AgdaAny -> Bool
forall a b. a -> b
coe Integer -> Integer -> Bool
geqInt (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer)) ->
                              (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_180
 -> T__'60''8314'__20
 -> T_Tree_180)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                   T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_180
-> T__'60''8314'__20
-> T_Tree_180
du_cast'691'_316 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v3) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
                                   (T__'60''8314'__20 -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20
v11))
                          AgdaAny
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12
                   T__'8764'_'8852'__30
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v12)
         T_Tree_180
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v10)
-- Data.Tree.AVL.Indexed._.empty
d_empty_790 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_180
d_empty_790 :: T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_180
d_empty_790 ~T_Value_38
v0 ~Maybe (Maybe AgdaAny)
v1 ~Maybe (Maybe AgdaAny)
v2 = T__'60''8314'__20 -> T_Tree_180
du_empty_790
du_empty_790 ::
  MAlonzo.Code.Relation.Binary.Construct.Add.Supremum.Strict.T__'60''8314'__20 ->
  T_Tree_180
du_empty_790 :: T__'60''8314'__20 -> T_Tree_180
du_empty_790 = (T__'60''8314'__20 -> T_Tree_180)
-> T__'60''8314'__20 -> T_Tree_180
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192
-- Data.Tree.AVL.Indexed._.singleton
d_singleton_798 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_180
d_singleton_798 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Σ_14
-> T_Tree_180
d_singleton_798 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
  = AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 AgdaAny
v8 AgdaAny
v9 T_Σ_14
v10
du_singleton_798 ::
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Tree_180
du_singleton_798 :: AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 AgdaAny
v0 AgdaAny
v1 T_Σ_14
v2
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
        -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_180
forall a b. a -> b
coe
             Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 (Integer
0 :: Integer) (Integer
0 :: Integer)
             ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1))
             ((T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)) ((T__'60''8314'__20 -> T_Tree_180) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'60''8314'__20 -> T_Tree_180
C_leaf_192 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
             (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
MAlonzo.Code.Data.Tree.AVL.Height.C_'8764'0_38)
      T_Σ_14
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insertWith
d_insertWith_818 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insertWith_818 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_insertWith_818 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_180
v11 T_Σ_14
v12
  = T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 T_StrictTotalOrder_1036
v3 T_Value_38
v5 AgdaAny
v9 Maybe AgdaAny -> AgdaAny
v10 T_Tree_180
v11 T_Σ_14
v12
du_insertWith_818 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny ->
  (Maybe AgdaAny -> AgdaAny) ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insertWith_818 :: T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 T_StrictTotalOrder_1036
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_180
v4 T_Σ_14
v5
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v4 of
      C_leaf_192 T__'60''8314'__20
v6
        -> (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
             ((T_Fin_10 -> T_Fin_10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Fin_10 -> T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_suc_16
                (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12))
             ((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_180
du_singleton_798 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
                ((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v5))
      C_node_208 Integer
v6 Integer
v7 T_K'38'__56
v9 T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v9 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v13 AgdaAny
v14
               -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v5 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v15 AgdaAny
v16
                      -> let v17 :: t
v17
                               = (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
                                   (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))
                                   AgdaAny
v2 AgdaAny
v13 in
                         AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v17 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v18
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8314'_366 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9)
                                     ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3)
                                        (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10)
                                        ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)
                                           ((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
                                              ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                 AgdaAny
v18))))
                                     (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v19
                                -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                     (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12)
                                     ((Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v6 Integer
v7
                                        ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                           ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                              T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v2
                                              AgdaAny
v13 AgdaAny
v19
                                              ((Maybe AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 Maybe AgdaAny -> AgdaAny
v3
                                                 ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                    ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                       T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48
                                                       T_Value_38
v1 AgdaAny
v13 AgdaAny
v2
                                                       (let v21 :: t
v21
                                                              = (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 v22 :: t
v22
                                                                 = (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
v21) in
                                                           AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                             (let v23 :: t
v23
                                                                    = (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
v22) in
                                                              AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                                ((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_Setoid_44 -> T_IsEquivalence_26
MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60
                                                                      (AgdaAny -> T_Setoid_44
forall a b. a -> b
coe AgdaAny
forall a. a
v23))
                                                                   AgdaAny
v2 AgdaAny
v13 AgdaAny
v19))))
                                                       AgdaAny
v14)))))
                                        T_Tree_180
v10 T_Tree_180
v11 T__'8764'_'8852'__30
v12)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v20
                                -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                     Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8314'_456 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v6) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v9) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10)
                                     ((T_StrictTotalOrder_1036
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny -> AgdaAny
v3)
                                        (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
                                        ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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
                                              ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                 AgdaAny
v20))
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)))
                                     (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v12)
                              T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__56
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.insert
d_insert_920 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_insert_920 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_insert_920 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 AgdaAny
v9 AgdaAny
v10
  = T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insert_920 T_StrictTotalOrder_1036
v3 T_Value_38
v5 AgdaAny
v9 AgdaAny
v10
du_insert_920 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny ->
  AgdaAny ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_insert_920 :: T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insert_920 T_StrictTotalOrder_1036
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3
  = (T_StrictTotalOrder_1036
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
forall a b. a -> b
coe
      T_StrictTotalOrder_1036
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_insertWith_818 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL.Indexed._.delete
d_delete_936 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_delete_936 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
d_delete_936 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_180
v10 T_Σ_14
v11
  = T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 T_StrictTotalOrder_1036
v3 Maybe (Maybe AgdaAny)
v6 Maybe (Maybe AgdaAny)
v7 Integer
v8 AgdaAny
v9 T_Tree_180
v10 T_Σ_14
v11
du_delete_936 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  AgdaAny ->
  T_Tree_180 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_delete_936 :: T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 T_StrictTotalOrder_1036
v0 Maybe (Maybe AgdaAny)
v1 Maybe (Maybe AgdaAny)
v2 Integer
v3 AgdaAny
v4 T_Tree_180
v5 T_Σ_14
v6
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v5 of
      C_leaf_192 T__'60''8314'__20
v7
        -> (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
             (T_Fin_10 -> AgdaAny
forall a b. a -> b
coe T_Fin_10
MAlonzo.Code.Data.Fin.Base.C_zero_12) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v5)
      C_node_208 Integer
v7 Integer
v8 T_K'38'__56
v10 T_Tree_180
v11 T_Tree_180
v12 T__'8764'_'8852'__30
v13
        -> let v14 :: Integer
v14 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v3) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> T_Σ_14
forall a b. a -> b
coe
             (case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v10 of
                MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v15 AgdaAny
v16
                  -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v6 of
                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v17 AgdaAny
v18
                         -> let v19 :: t
v19
                                  = (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                      T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
                                      (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))
                                      AgdaAny
v15 AgdaAny
v4 in
                            AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v19 of
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v20
                                   -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Σ_14
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Σ_14
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'691''8315'_594 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
                                        ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0)
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                           (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12)
                                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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
                                                 ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                    AgdaAny
v20))
                                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v18)))
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v21
                                   -> (T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> Integer
 -> Integer
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> Integer
-> Integer
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join_754 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                                        ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                        (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v14) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12)
                                        (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v22
                                   -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Σ_14
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        Integer
-> Integer
-> T_K'38'__56
-> T_Σ_14
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Σ_14
du_join'737''8315'_532 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v8) (T_K'38'__56 -> AgdaAny
forall a b. a -> b
coe T_K'38'__56
v10)
                                        ((T_StrictTotalOrder_1036
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_180
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                           T_StrictTotalOrder_1036
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_180
-> T_Σ_14
-> T_Σ_14
du_delete_936 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (Maybe (Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe Maybe (Maybe AgdaAny)
v1)
                                           ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                              ((AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                                 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15)))
                                           (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v7) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v11)
                                           ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17)
                                              ((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
                                                 ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                                    AgdaAny
v22))))
                                        (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v12) (T__'8764'_'8852'__30 -> AgdaAny
forall a b. a -> b
coe T__'8764'_'8852'__30
v13)
                                 T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                       T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
      T_Tree_180
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.lookup
d_lookup_1034 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_180 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
d_lookup_1034 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> AgdaAny
-> T_Σ_14
-> Maybe AgdaAny
d_lookup_1034 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9 AgdaAny
v10 T_Σ_14
v11
  = T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 T_StrictTotalOrder_1036
v3 T_Value_38
v5 T_Tree_180
v9 AgdaAny
v10 T_Σ_14
v11
du_lookup_1034 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_180 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 :: T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 T_StrictTotalOrder_1036
v0 T_Value_38
v1 T_Tree_180
v2 AgdaAny
v3 T_Σ_14
v4
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v2 of
      C_leaf_192 T__'60''8314'__20
v5 -> Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
      C_node_208 Integer
v5 Integer
v6 T_K'38'__56
v8 T_Tree_180
v9 T_Tree_180
v10 T__'8764'_'8852'__30
v11
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v8 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v12 AgdaAny
v13
               -> case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v4 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v14 AgdaAny
v15
                      -> let v16 :: t
v16
                               = (T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158)
-> T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                   T_IsStrictTotalOrder_534 -> AgdaAny -> AgdaAny -> T_Tri_158
MAlonzo.Code.Relation.Binary.Structures.d_compare_544
                                   (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))
                                   AgdaAny
v12 AgdaAny
v3 in
                         AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
                           (case AgdaAny -> T_Tri_158
forall a b. a -> b
coe AgdaAny
forall a. a
v16 of
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'60'_172 AgdaAny
v17
                                -> (T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v10) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
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
                                           ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                              AgdaAny
v17))
                                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'8776'_180 AgdaAny
v18
                                -> (AgdaAny -> Maybe AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16
                                     ((T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Value.d_respects_48 T_Value_38
v1 AgdaAny
v12 AgdaAny
v3 AgdaAny
v18
                                        AgdaAny
v13)
                              MAlonzo.Code.Relation.Binary.Definitions.C_tri'62'_188 AgdaAny
v19
                                -> (T_StrictTotalOrder_1036
 -> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_StrictTotalOrder_1036
-> T_Value_38 -> T_Tree_180 -> AgdaAny -> T_Σ_14 -> Maybe AgdaAny
du_lookup_1034 (T_StrictTotalOrder_1036 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_1036
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v9) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                        ((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
                                           ((AgdaAny -> T__'60''8331'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              AgdaAny -> T__'60''8331'__20
MAlonzo.Code.Relation.Binary.Construct.Add.Infimum.Strict.C_'91'_'93'_30
                                              AgdaAny
v19)))
                              T_Tri_158
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
                    T_Σ_14
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_K'38'__56
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_180
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.foldr
d_foldr_1114 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_180 -> AgdaAny
d_foldr_1114 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> T_Level_18
-> T_Level_18
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_180
-> AgdaAny
d_foldr_1114 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~T_Level_18
v6 ~T_Level_18
v7 ~Maybe (Maybe AgdaAny)
v8 ~Maybe (Maybe AgdaAny)
v9 ~Integer
v10 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12
             T_Tree_180
v13
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v11 AgdaAny
v12 T_Tree_180
v13
du_foldr_1114 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_180
v2
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v2 of
      C_leaf_192 T__'60''8314'__20
v3 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      C_node_208 Integer
v3 Integer
v4 T_K'38'__56
v6 T_Tree_180
v7 T_Tree_180
v8 T__'8764'_'8852'__30
v9
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v6 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v10 AgdaAny
v11
               -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_180 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0)
                    ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v10 AgdaAny
v11 (((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_180 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_180 -> AgdaAny
du_foldr_1114 ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v8)))
                    (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)
             T_K'38'__56
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_180
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toDiffList
d_toDiffList_1140 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_180 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toDiffList_1140 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> [T_K'38'__56]
-> [T_K'38'__56]
d_toDiffList_1140 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
  = T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v9
du_toDiffList_1140 ::
  T_Tree_180 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toDiffList_1140 :: T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v0
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v0 of
      C_leaf_192 T__'60''8314'__20
v1 -> (AgdaAny -> AgdaAny) -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe (\ AgdaAny
v2 -> AgdaAny
v2)
      C_node_208 Integer
v1 Integer
v2 T_K'38'__56
v4 T_Tree_180
v5 T_Tree_180
v6 T__'8764'_'8852'__30
v7
        -> (([AgdaAny] -> [AgdaAny])
 -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> [T_K'38'__56] -> [T_K'38'__56]
forall a b. a -> b
coe
             ([AgdaAny] -> [AgdaAny])
-> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'43''43'__38
             ((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v5))
             ((AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny])
-> T_K'38'__56 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> ([AgdaAny] -> [AgdaAny]) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du__'8759'__28 T_K'38'__56
v4
                ((T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6)))
      T_Tree_180
_ -> [T_K'38'__56] -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL.Indexed._.toList
d_toList_1154 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Integer ->
  T_Tree_180 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_1154 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> [T_K'38'__56]
d_toList_1154 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 T_Tree_180
v9
  = T_Tree_180 -> [T_K'38'__56]
du_toList_1154 T_Tree_180
v9
du_toList_1154 ::
  T_Tree_180 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_1154 :: T_Tree_180 -> [T_K'38'__56]
du_toList_1154 T_Tree_180
v0
  = (T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56])
-> T_Tree_180 -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
      T_Tree_180 -> [T_K'38'__56] -> [T_K'38'__56]
du_toDiffList_1140 T_Tree_180
v0
      ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
-- Data.Tree.AVL.Indexed._.size
d_size_1164 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_180 -> Integer
d_size_1164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Value_38
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> Integer
d_size_1164 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Value_38
v5 ~Maybe (Maybe AgdaAny)
v6 ~Maybe (Maybe AgdaAny)
v7 ~Integer
v8 = T_Tree_180 -> Integer
du_size_1164
du_size_1164 :: T_Tree_180 -> Integer
du_size_1164 :: T_Tree_180 -> Integer
du_size_1164
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> T_Tree_180 -> Integer
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__216
      (([AgdaAny] -> Integer) -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> Integer
MAlonzo.Code.Data.List.Base.du_length_284)
      ((T_Tree_180 -> [T_K'38'__56]) -> AgdaAny
forall a b. a -> b
coe T_Tree_180 -> [T_K'38'__56]
du_toList_1154)
-- Data.Tree.AVL.Indexed._.Val
d_Val_1178 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_1178 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Val_1178 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.Wal
d_Wal_1180 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_1036 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_1180 :: T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
d_Wal_1180 = T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> T_Level_18
forall a. a
erased
-- Data.Tree.AVL.Indexed._.map
d_map_1188 ::
  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.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe (Maybe AgdaAny) ->
  Maybe (Maybe AgdaAny) -> Integer -> T_Tree_180 -> T_Tree_180
d_map_1188 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_StrictTotalOrder_1036
-> T_Level_18
-> T_Level_18
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> T_Tree_180
-> T_Tree_180
d_map_1188 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_StrictTotalOrder_1036
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~T_Value_38
v6 ~T_Value_38
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 ~Maybe (Maybe AgdaAny)
v9 ~Maybe (Maybe AgdaAny)
v10 ~Integer
v11 T_Tree_180
v12
  = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_180
v12
du_map_1188 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_180
v1
  = case T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1 of
      C_leaf_192 T__'60''8314'__20
v2 -> T_Tree_180 -> T_Tree_180
forall a b. a -> b
coe T_Tree_180
v1
      C_node_208 Integer
v2 Integer
v3 T_K'38'__56
v5 T_Tree_180
v6 T_Tree_180
v7 T__'8764'_'8852'__30
v8
        -> case T_K'38'__56 -> T_K'38'__56
forall a b. a -> b
coe T_K'38'__56
v5 of
             MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 AgdaAny
v9 AgdaAny
v10
               -> (Integer
 -> Integer
 -> T_K'38'__56
 -> T_Tree_180
 -> T_Tree_180
 -> T__'8764'_'8852'__30
 -> T_Tree_180)
-> Integer
-> Integer
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8764'_'8852'__30
-> T_Tree_180
forall a b. a -> b
coe
                    Integer
-> Integer
-> T_K'38'__56
-> T_Tree_180
-> T_Tree_180
-> T__'8764'_'8852'__30
-> T_Tree_180
C_node_208 Integer
v2 Integer
v3
                    ((AgdaAny -> AgdaAny -> T_K'38'__56)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_K'38'__56
MAlonzo.Code.Data.Tree.AVL.Value.C__'44'__70 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)
                       ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v9 AgdaAny
v10))
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v6))
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_180 -> T_Tree_180
du_map_1188 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_180 -> AgdaAny
forall a b. a -> b
coe T_Tree_180
v7)) T__'8764'_'8852'__30
v8
             T_K'38'__56
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Tree_180
_ -> T_Tree_180
forall a. a
MAlonzo.RTE.mazUnreachableError