{-# 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 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.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.List.Base
import qualified MAlonzo.Code.Data.Maybe.Base
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Data.Tree.AVL.Height
import qualified MAlonzo.Code.Data.Tree.AVL.Indexed
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.Supremum.Strict

-- Data.Tree.AVL.Indexed.K&_
d_K'38'__92 :: p -> p -> p -> p -> p -> p -> ()
d_K'38'__92 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
-- Data.Tree.AVL.Indexed.Tree
d_Tree_98 :: p -> p -> p -> p -> p -> p -> p -> p -> p -> ()
d_Tree_98 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 p
a6 p
a7 p
a8 = ()
-- Data.Tree.AVL.Indexed.Value
d_Value_100 :: p -> p -> p -> p -> p -> ()
d_Value_100 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
-- Data.Tree.AVL.Indexed.const
d_const_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
d_const_106 :: () -> () -> () -> T_StrictTotalOrder_864 -> () -> () -> T_Value_38
d_const_106 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 = () -> () -> T_Value_38
du_const_106
du_const_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38
du_const_106 :: () -> () -> T_Value_38
du_const_106 ()
v0 ()
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_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_864 ->
  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_114 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Σ_14
-> T_K'38'__56
d_fromPair_114 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 = () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_114
du_fromPair_114 ::
  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_114 :: () -> T_Value_38 -> T_Σ_14 -> T_K'38'__56
du_fromPair_114 ()
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.toPair
d_toPair_168 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_toPair_168 :: T_K'38'__56 -> T_Σ_14
d_toPair_168 = (T_K'38'__56 -> T_Σ_14) -> T_K'38'__56 -> T_Σ_14
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80
-- Data.Tree.AVL.Indexed.K&_.key
d_key_190 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_key_190 :: T_K'38'__56 -> AgdaAny
d_key_190 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_192 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56 -> AgdaAny
d_value_192 :: T_K'38'__56 -> AgdaAny
d_value_192 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_202 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_family_202 :: T_Value_38 -> AgdaAny -> ()
d_family_202 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL.Indexed.Value.respects
d_respects_204 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_204 :: T_Value_38 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
d_respects_204 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.Tree
d_Tree_240 :: p -> p -> p -> p -> p -> p -> ()
d_Tree_240 p
a0 p
a1 p
a2 p
a3 p
a4 p
a5 = ()
data T_Tree_240
  = C_tree_248 Integer MAlonzo.Code.Data.Tree.AVL.Indexed.T_Tree_166
-- Data.Tree.AVL._.Val
d_Val_258 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_258 :: T_Value_38 -> AgdaAny -> ()
d_Val_258 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.empty
d_empty_260 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> T_Tree_240
d_empty_260 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
d_empty_260 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 = T_Tree_240
du_empty_260
du_empty_260 :: T_Tree_240
du_empty_260 :: T_Tree_240
du_empty_260
  = let v0 :: t
v0 = (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
0 :: Integer)) in
    AgdaAny -> T_Tree_240
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny
forall a. a
v0
         ((T__'60''8314'__20 -> T_Tree_166) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T__'60''8314'__20 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178
            (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._.singleton
d_singleton_264 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_240
d_singleton_264 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_240
d_singleton_264 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 AgdaAny
v6 AgdaAny
v7
  = AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 AgdaAny
v6 AgdaAny
v7
du_singleton_264 :: AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 :: AgdaAny -> AgdaAny -> T_Tree_240
du_singleton_264 AgdaAny
v0 AgdaAny
v1
  = (Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
      Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe (Integer
1 :: Integer))
      ((AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> AgdaAny -> T_Σ_14 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_singleton_784 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0)
         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1)
         ((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
               (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._.insert
d_insert_272 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
d_insert_272 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_insert_272 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_240
v8
  = T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 AgdaAny
v7 T_Tree_240
v8
du_insert_272 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_240
v4
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v4 of
      C_tree_248 Integer
v5 T_Tree_166
v6
        -> let v7 :: t
v7
                 = (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
                     ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_166
v6
                              ((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
                                    (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))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
           AgdaAny -> T_Tree_240
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
forall a. a
v7
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insert_906 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 AgdaAny
v3 T_Tree_166
v6
                      ((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
                            (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)))))
      T_Tree_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.insertWith
d_insertWith_282 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
d_insertWith_282 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_insertWith_282 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_240
v8
  = T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 Maybe AgdaAny -> AgdaAny
v7 T_Tree_240
v8
du_insertWith_282 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> (Maybe AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_insertWith_282 :: T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 Maybe AgdaAny -> AgdaAny
v3 T_Tree_240
v4
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v4 of
      C_tree_248 Integer
v5 T_Tree_166
v6
        -> let v7 :: t
v7
                 = (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
                     ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)
                              ((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
                                    (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))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v5)) in
           AgdaAny -> T_Tree_240
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
forall a. a
v7
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_insertWith_804 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v6)
                      ((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
                            (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)))))
      T_Tree_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.delete
d_delete_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_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_240 -> T_Tree_240
d_delete_290 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_delete_290 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7 = T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 T_StrictTotalOrder_864
v3 AgdaAny
v6 T_Tree_240
v7
du_delete_290 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 :: T_StrictTotalOrder_864 -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_delete_290 T_StrictTotalOrder_864
v0 AgdaAny
v1 T_Tree_240
v2
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v2 of
      C_tree_248 Integer
v3 T_Tree_166
v4
        -> let v5 :: t
v5
                 = (Integer -> T_Tree_166 -> T_Tree_240) -> AgdaAny -> t
forall a b. a -> b
coe
                     Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
                     ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d_pred'91'_'8853'_'93'_22
                        ((T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                           ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                              T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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
                                 (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                              (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
                              ((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
                                    (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))))
                        (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)) in
           AgdaAny -> T_Tree_240
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny
forall a. a
v5
                (T_Σ_14 -> AgdaAny
MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                   ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Integer
 -> AgdaAny
 -> T_Tree_166
 -> T_Σ_14
 -> T_Σ_14)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Σ_14
forall a b. a -> b
coe
                      T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Integer
-> AgdaAny
-> T_Tree_166
-> T_Σ_14
-> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_delete_922 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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
                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                      (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3)
                      (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
                      ((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
                            (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)))))
      T_Tree_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.lookup
d_lookup_298 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_240 -> Maybe AgdaAny
d_lookup_298 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> Maybe AgdaAny
d_lookup_298 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
  = T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
du_lookup_298 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_240
v3
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v3 of
      C_tree_248 Integer
v4 T_Tree_166
v5
        -> (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> Maybe AgdaAny
forall a b. a -> b
coe
             T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_166 -> T_Σ_14 -> Maybe AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_lookup_1020 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
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
                ((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))
      T_Tree_240
_ -> Maybe AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_316 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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_316 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Val_316 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_318 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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_318 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Wal_318 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.map
d_map_320 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.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) -> T_Tree_240 -> T_Tree_240
d_map_320 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
d_map_320 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 ~T_Value_38
v7 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_240
v9 = (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 AgdaAny -> AgdaAny -> AgdaAny
v8 T_Tree_240
v9
du_map_320 ::
  (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 :: (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_240 -> T_Tree_240
du_map_320 AgdaAny -> AgdaAny -> AgdaAny
v0 T_Tree_240
v1
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
      C_tree_248 Integer
v2 T_Tree_166
v3
        -> (Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
             Integer -> T_Tree_166 -> T_Tree_240
C_tree_248 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2)
             (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                (AgdaAny -> AgdaAny -> AgdaAny) -> T_Tree_166 -> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_map_1174 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0) (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3))
      T_Tree_240
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_334 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_334 :: T_Value_38 -> AgdaAny -> ()
d_Val_334 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._._∈?_
d__'8712''63'__336 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_240 -> Bool
d__'8712''63'__336 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> AgdaAny
-> T_Tree_240
-> Bool
d__'8712''63'__336 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
  = T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny
v6 T_Tree_240
v7
du__'8712''63'__336 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 :: T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Bool
du__'8712''63'__336 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny
v2 T_Tree_240
v3
  = (Maybe AgdaAny -> Bool) -> AgdaAny -> Bool
forall a b. a -> b
coe
      Maybe AgdaAny -> Bool
MAlonzo.Code.Data.Maybe.Base.du_is'45'just_20
      ((T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v3))
-- Data.Tree.AVL._.headTail
d_headTail_342 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_headTail_342 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Maybe T_Σ_14
d_headTail_342 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_342 T_StrictTotalOrder_864
v3 T_Tree_240
v6
du_headTail_342 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_headTail_342 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_headTail_342 T_StrictTotalOrder_864
v0 T_Tree_240
v1
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
      C_tree_248 Integer
v2 T_Tree_166
v3
        -> let v4 :: b
v4
                 = let v4 :: Integer
v4 = 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 v5 :: t
v5
                            = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                Integer -> T_Tree_166 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_headTail_634 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                                    -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                                           -> (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 -> 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
v6)
                                                   ((Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                      Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
                                                      ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T__'60''8314'__20
 -> T_Tree_166
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T__'60''8314'__20
-> T_Tree_166
-> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'737'_276
                                                         (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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
                                                            (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((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
v6))))
                                                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         ((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))
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11))))
                                         T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178 T__'60''8314'__20
v5
                  -> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)
      T_Tree_240
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.initLast
d_initLast_356 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_initLast_356 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Maybe T_Σ_14
d_initLast_356 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_356 T_StrictTotalOrder_864
v3 T_Tree_240
v6
du_initLast_356 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  T_Tree_240 -> Maybe MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_initLast_356 :: T_StrictTotalOrder_864 -> T_Tree_240 -> Maybe T_Σ_14
du_initLast_356 T_StrictTotalOrder_864
v0 T_Tree_240
v1
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v1 of
      C_tree_248 Integer
v2 T_Tree_166
v3
        -> let v4 :: b
v4
                 = let v4 :: Integer
v4 = 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 v5 :: t
v5
                            = (Integer -> T_Tree_166 -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe
                                Integer -> T_Tree_166 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Indexed.du_initLast_684 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4)
                                (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v3) in
                      AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        (case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
forall a. a
v5 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v6 AgdaAny
v7
                             -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v7 of
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                                    -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                                           -> (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 -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                   ((Integer -> T_Tree_166 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                      Integer -> T_Tree_166 -> T_Tree_240
C_tree_248
                                                      ((T_Fin_6 -> Integer -> Integer) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                         T_Fin_6 -> Integer -> Integer
MAlonzo.Code.Data.Tree.AVL.Height.d__'8853'__16
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                                                      ((T_StrictTotalOrder_864
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> Maybe (Maybe AgdaAny)
 -> T_Tree_166
 -> T__'60''8314'__20
 -> T_Tree_166)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                         T_StrictTotalOrder_864
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> Maybe (Maybe AgdaAny)
-> T_Tree_166
-> T__'60''8314'__20
-> T_Tree_166
MAlonzo.Code.Data.Tree.AVL.Indexed.du_cast'691'_302
                                                         (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
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
                                                            (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                               Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18))
                                                         ((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
v6))))
                                                         (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                            Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18)
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11)
                                                         (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)))
                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
                                         T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                                  T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)) in
           AgdaAny -> Maybe T_Σ_14
forall a b. a -> b
coe
             (case T_Tree_166 -> T_Tree_166
forall a b. a -> b
coe T_Tree_166
v3 of
                MAlonzo.Code.Data.Tree.AVL.Indexed.C_leaf_178 T__'60''8314'__20
v5
                  -> Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                T_Tree_166
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v4)
      T_Tree_240
_ -> Maybe T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.foldr
d_foldr_372 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_240 -> AgdaAny
d_foldr_372 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> ()
-> ()
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Tree_240
-> AgdaAny
d_foldr_372 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 ~()
v6 ~()
v7 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_240
v10
  = (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v8 AgdaAny
v9 T_Tree_240
v10
du_foldr_372 ::
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 :: (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v1 T_Tree_240
v2
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v2 of
      C_tree_248 Integer
v3 T_Tree_166
v4
        -> ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_166 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_166 -> AgdaAny
MAlonzo.Code.Data.Tree.AVL.Indexed.du_foldr_1100 ((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_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v4)
      T_Tree_240
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.fromList
d_fromList_380 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_240
d_fromList_380 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_K'38'__56]
-> T_Tree_240
d_fromList_380 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864 -> T_Value_38 -> [T_K'38'__56] -> T_Tree_240
du_fromList_380 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_fromList_380 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56] -> T_Tree_240
du_fromList_380 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_K'38'__56] -> T_Tree_240
du_fromList_380 T_StrictTotalOrder_864
v0 T_Value_38
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> [T_K'38'__56] -> T_Tree_240
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
MAlonzo.Code.Function.Base.du__'8728''8242'__226
         (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.du_uncurry_264
            ((T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1)))
         ((T_K'38'__56 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T_K'38'__56 -> T_Σ_14
MAlonzo.Code.Data.Tree.AVL.Value.d_toPair_80))
      (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260)
-- Data.Tree.AVL._.toList
d_toList_382 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
d_toList_382 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> [T_K'38'__56]
d_toList_382 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_Tree_240 -> [T_K'38'__56]
du_toList_382 T_Tree_240
v6
du_toList_382 ::
  T_Tree_240 -> [MAlonzo.Code.Data.Tree.AVL.Value.T_K'38'__56]
du_toList_382 :: T_Tree_240 -> [T_K'38'__56]
du_toList_382 T_Tree_240
v0
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v0 of
      C_tree_248 Integer
v1 T_Tree_166
v2
        -> (([AgdaAny] -> [AgdaAny]) -> [AgdaAny]) -> AgdaAny -> [T_K'38'__56]
forall a b. a -> b
coe
             ([AgdaAny] -> [AgdaAny]) -> [AgdaAny]
MAlonzo.Code.Data.DifferenceList.du_toList_54
             ((T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56])
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Tree_166 -> [T_K'38'__56] -> [T_K'38'__56]
MAlonzo.Code.Data.Tree.AVL.Indexed.du_toDiffList_1126 (T_Tree_166 -> AgdaAny
forall a b. a -> b
coe T_Tree_166
v2))
      T_Tree_240
_ -> [T_K'38'__56]
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.size
d_size_386 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> Integer
d_size_386 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> Integer
d_size_386 ~()
v0 ~()
v1 ~()
v2 ~T_StrictTotalOrder_864
v3 ~()
v4 ~T_Value_38
v5 T_Tree_240
v6 = T_Tree_240 -> Integer
du_size_386 T_Tree_240
v6
du_size_386 :: T_Tree_240 -> Integer
du_size_386 :: T_Tree_240 -> Integer
du_size_386 T_Tree_240
v0
  = case T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
v0 of
      C_tree_248 Integer
v1 T_Tree_166
v2
        -> (T_Tree_166 -> Integer) -> T_Tree_166 -> Integer
forall a b. a -> b
coe T_Tree_166 -> Integer
MAlonzo.Code.Data.Tree.AVL.Indexed.du_size_1150 T_Tree_166
v2
      T_Tree_240
_ -> Integer
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.Val
d_Val_402 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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_402 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Val_402 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_404 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  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_404 :: T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
d_Wal_404 = T_StrictTotalOrder_864
-> () -> () -> T_Value_38 -> T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.unionWith
d_unionWith_408 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.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 -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_unionWith_408 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_unionWith_408 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~T_Value_38
v6 T_Value_38
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_240
v9 T_Tree_240
v10
  = T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 T_StrictTotalOrder_864
v3 T_Value_38
v7 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v8 T_Tree_240
v9 T_Tree_240
v10
du_unionWith_408 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_unionWith_408 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 T_Tree_240
v3 T_Tree_240
v4
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_240 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v5 AgdaAny
v6 ->
            (T_StrictTotalOrder_864
 -> T_Value_38
 -> AgdaAny
 -> (Maybe AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> AgdaAny
-> (Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
du_insertWith_282 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 AgdaAny
v5 AgdaAny
v6)))
      (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v3)
-- Data.Tree.AVL._.Val
d_Val_428 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_428 :: T_Value_38 -> AgdaAny -> ()
d_Val_428 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.union
d_union_430 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_union_430 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_union_430 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_union_430 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 :: T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_union_430 T_StrictTotalOrder_864
v0 T_Value_38
v1
  = (T_StrictTotalOrder_864
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.unionsWith
d_unionsWith_434 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_240] -> T_Tree_240
d_unionsWith_434 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_unionsWith_434 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
  = T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
du_unionsWith_434 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) ->
  [T_Tree_240] -> T_Tree_240
du_unionsWith_434 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2 [T_Tree_240]
v3
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_240
      ((T_StrictTotalOrder_864
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_unionWith_408 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny
v2))
      (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260) ([T_Tree_240] -> AgdaAny
forall a b. a -> b
coe [T_Tree_240]
v3)
-- Data.Tree.AVL._.unions
d_unions_440 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_240] -> T_Tree_240
d_unions_440 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_Tree_240]
-> T_Tree_240
d_unions_440 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 = T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_unions_440 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_unions_440 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_240] -> T_Tree_240
du_unions_440 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_unions_440 T_StrictTotalOrder_864
v0 T_Value_38
v1
  = (T_StrictTotalOrder_864
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
 -> [T_Tree_240]
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> Maybe AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_unionsWith_434 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.Val
d_Val_458 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_458 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Val_458 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Wal
d_Wal_460 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Wal_460 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Wal_460 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.Xal
d_Xal_462 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Xal_462 :: T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
d_Xal_462 = T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> AgdaAny
-> ()
forall a. a
erased
-- Data.Tree.AVL._.intersectionWith
d_intersectionWith_466 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_intersectionWith_466 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersectionWith_466 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v11
                       T_Tree_240
v12
  = T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 T_StrictTotalOrder_864
v3 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v11 T_Tree_240
v12
du_intersectionWith_466 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersectionWith_466 :: T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 T_StrictTotalOrder_864
v0 T_Value_38
v1 T_Value_38
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_240
v4 T_Tree_240
v5
  = ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> T_Tree_240 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> T_Tree_240 -> AgdaAny
du_foldr_372
      ((T_StrictTotalOrder_864
 -> T_Value_38
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> AgdaAny
 -> AgdaAny
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v2) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v5))
      (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
du_empty_260) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4)
-- Data.Tree.AVL._._.cons
d_cons_480 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  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 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_240 ->
  T_Tree_240 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
d_cons_480 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> ()
-> ()
-> T_Value_38
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
d_cons_480 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 ~()
v5 ~()
v6 ~T_Value_38
v7 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 ~T_Tree_240
v11 T_Tree_240
v12 AgdaAny
v13
           AgdaAny
v14
  = T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 T_StrictTotalOrder_864
v3 T_Value_38
v8 T_Value_38
v9 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v10 T_Tree_240
v12 AgdaAny
v13 AgdaAny
v14
du_cons_480 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  T_Tree_240 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_cons_480 :: T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
du_cons_480 T_StrictTotalOrder_864
v0 T_Value_38
v1 T_Value_38
v2 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 T_Tree_240
v4 AgdaAny
v5 AgdaAny
v6
  = let v7 :: t
v7 = (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> t
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> T_Tree_240 -> Maybe AgdaAny
du_lookup_298 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (T_Tree_240 -> AgdaAny
forall a b. a -> b
coe T_Tree_240
v4) in
    AgdaAny -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe
      (case AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v7 of
         MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v8
           -> (T_StrictTotalOrder_864
 -> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38 -> AgdaAny -> AgdaAny -> T_Tree_240 -> T_Tree_240
du_insert_272 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v3 AgdaAny
v5 AgdaAny
v6 AgdaAny
v8)
         Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 -> (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v8 -> AgdaAny
v8)
         Maybe AgdaAny
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- Data.Tree.AVL._.Val
d_Val_498 ::
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 -> AgdaAny -> ()
d_Val_498 :: T_Value_38 -> AgdaAny -> ()
d_Val_498 = T_Value_38 -> AgdaAny -> ()
forall a. a
erased
-- Data.Tree.AVL._.intersection
d_intersection_500 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
d_intersection_500 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
d_intersection_500 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5
  = T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_intersection_500 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 :: T_StrictTotalOrder_864
-> T_Value_38 -> T_Tree_240 -> T_Tree_240 -> T_Tree_240
du_intersection_500 T_StrictTotalOrder_864
v0 T_Value_38
v1
  = (T_StrictTotalOrder_864
 -> T_Value_38
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
forall a b. a -> b
coe
      T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1)
      ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))
-- Data.Tree.AVL._.intersectionsWith
d_intersectionsWith_504 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_240] -> T_Tree_240
d_intersectionsWith_504 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
d_intersectionsWith_504 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
  = T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 T_StrictTotalOrder_864
v3 T_Value_38
v5 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v6 [T_Tree_240]
v7
du_intersectionsWith_504 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
  [T_Tree_240] -> T_Tree_240
du_intersectionsWith_504 :: T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 T_StrictTotalOrder_864
v0 T_Value_38
v1 AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2 [T_Tree_240]
v3
  = case [T_Tree_240] -> [AgdaAny]
forall a b. a -> b
coe [T_Tree_240]
v3 of
      [] -> T_Tree_240 -> T_Tree_240
forall a b. a -> b
coe T_Tree_240
du_empty_260
      (:) AgdaAny
v4 [AgdaAny]
v5
        -> ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Tree_240
forall a b. a -> b
coe
             (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldl_254
             ((T_StrictTotalOrder_864
 -> T_Value_38
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> T_Tree_240
 -> T_Tree_240
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
-> T_Value_38
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> T_Tree_240
-> T_Tree_240
-> T_Tree_240
du_intersectionWith_466 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
v2))
             (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5)
      [AgdaAny]
_ -> T_Tree_240
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Tree.AVL._.intersections
d_intersections_514 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_240] -> T_Tree_240
d_intersections_514 :: ()
-> ()
-> ()
-> T_StrictTotalOrder_864
-> ()
-> T_Value_38
-> [T_Tree_240]
-> T_Tree_240
d_intersections_514 ~()
v0 ~()
v1 ~()
v2 T_StrictTotalOrder_864
v3 ~()
v4 T_Value_38
v5
  = T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_intersections_514 T_StrictTotalOrder_864
v3 T_Value_38
v5
du_intersections_514 ::
  MAlonzo.Code.Relation.Binary.Bundles.T_StrictTotalOrder_864 ->
  MAlonzo.Code.Data.Tree.AVL.Value.T_Value_38 ->
  [T_Tree_240] -> T_Tree_240
du_intersections_514 :: T_StrictTotalOrder_864 -> T_Value_38 -> [T_Tree_240] -> T_Tree_240
du_intersections_514 T_StrictTotalOrder_864
v0 T_Value_38
v1
  = (T_StrictTotalOrder_864
 -> T_Value_38
 -> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
 -> [T_Tree_240]
 -> T_Tree_240)
-> AgdaAny -> AgdaAny -> AgdaAny -> [T_Tree_240] -> T_Tree_240
forall a b. a -> b
coe
      T_StrictTotalOrder_864
-> T_Value_38
-> (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> [T_Tree_240]
-> T_Tree_240
du_intersectionsWith_504 (T_StrictTotalOrder_864 -> AgdaAny
forall a b. a -> b
coe T_StrictTotalOrder_864
v0) (T_Value_38 -> AgdaAny
forall a b. a -> b
coe T_Value_38
v1) ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v2 AgdaAny
v3 AgdaAny
v4 -> AgdaAny
v3))