content: {-# 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.List.Properties where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Bool qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.List qualified
  import MAlonzo.Code.Agda.Builtin.Maybe qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Algebra.Bundles qualified
  import MAlonzo.Code.Algebra.Morphism.Structures qualified
  import MAlonzo.Code.Algebra.Structures qualified
  import MAlonzo.Code.Data.Fin.Base qualified
  import MAlonzo.Code.Data.Irrelevant qualified
  import MAlonzo.Code.Data.List.Base qualified
  import MAlonzo.Code.Data.List.Relation.Unary.All qualified
  import MAlonzo.Code.Data.List.Relation.Unary.Any qualified
  import MAlonzo.Code.Data.Maybe.Relation.Unary.Any qualified
  import MAlonzo.Code.Data.Nat.Base qualified
  import MAlonzo.Code.Data.Nat.Divisibility qualified
  import MAlonzo.Code.Data.Nat.Divisibility.Core qualified
  import MAlonzo.Code.Data.Nat.Properties qualified
  import MAlonzo.Code.Data.Product.Base qualified
  import MAlonzo.Code.Data.Sum.Base qualified
  import MAlonzo.Code.Data.These.Base qualified
  import MAlonzo.Code.Relation.Binary.Morphism.Structures qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple qualified
  import MAlonzo.Code.Relation.Binary.Reasoning.Syntax qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
  import MAlonzo.Code.Relation.Nullary.Negation.Core qualified
  import MAlonzo.Code.Relation.Nullary.Reflects qualified
  import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                      mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                      word64ToNat)
  import MAlonzo.RTE qualified
  
  -- Data.List.Properties.∷-injective
  d_'8759''45'injective_46 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8759''45'injective_46 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6
    = du_'8759''45'injective_46
  du_'8759''45'injective_46 :: MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'8759''45'injective_46
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.List.Properties.∷-injectiveˡ
  d_'8759''45'injective'737'_48 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8759''45'injective'737'_48 = erased
  -- Data.List.Properties.∷-injectiveʳ
  d_'8759''45'injective'691'_50 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8759''45'injective'691'_50 = erased
  -- Data.List.Properties.∷-dec
  d_'8759''45'dec_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_'8759''45'dec_52 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
    = du_'8759''45'dec_52 v6 v7
  du_'8759''45'dec_52 ::
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_'8759''45'dec_52 v0 v1
    = coe
        MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
        (coe MAlonzo.Code.Data.Product.Base.du_uncurry_244 erased)
        (\ v2 -> coe du_'8759''45'injective_46)
        (coe
           MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
           (coe v0) (coe v1))
  -- Data.List.Properties.≡-dec
  d_'8801''45'dec_58 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_'8801''45'dec_58 ~v0 ~v1 v2 v3 v4 = du_'8801''45'dec_58 v2 v3 v4
  du_'8801''45'dec_58 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_'8801''45'dec_58 v0 v1 v2
    = case coe v1 of
        []
          -> case coe v2 of
               []
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               (:) v3 v4
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        (:) v3 v4
          -> case coe v2 of
               []
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               (:) v5 v6
                 -> coe
                      du_'8759''45'dec_52 (coe v0 v3 v5)
                      (coe du_'8801''45'dec_58 (coe v0) (coe v4) (coe v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.map-id
  d_map'45'id_84 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'id_84 = erased
  -- Data.List.Properties.map-id-local
  d_map'45'id'45'local_98 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'id'45'local_98 = erased
  -- Data.List.Properties.map-++
  d_map'45''43''43'_110 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''43''43'_110 = erased
  -- Data.List.Properties.map-cong
  d_map'45'cong_130 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'cong_130 = erased
  -- Data.List.Properties.map-cong-local
  d_map'45'cong'45'local_148 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'cong'45'local_148 = erased
  -- Data.List.Properties.length-map
  d_length'45'map_158 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'map_158 = erased
  -- Data.List.Properties.map-∘
  d_map'45''8728'_172 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''8728'_172 = erased
  -- Data.List.Properties.map-injective
  d_map'45'injective_182 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'injective_182 = erased
  -- Data.List.Properties.length-++
  d_length'45''43''43'_208 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45''43''43'_208 = erased
  -- Data.List.Properties._._.Associative
  d_Associative_246 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_Associative_246 = erased
  -- Data.List.Properties._._.Cancellative
  d_Cancellative_248 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_Cancellative_248 = erased
  -- Data.List.Properties._._.Conical
  d_Conical_256 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_Conical_256 = erased
  -- Data.List.Properties._._.Identity
  d_Identity_266 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_Identity_266 = erased
  -- Data.List.Properties._._.LeftCancellative
  d_LeftCancellative_280 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_LeftCancellative_280 = erased
  -- Data.List.Properties._._.LeftIdentity
  d_LeftIdentity_292 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_LeftIdentity_292 = erased
  -- Data.List.Properties._._.RightCancellative
  d_RightCancellative_310 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_RightCancellative_310 = erased
  -- Data.List.Properties._._.RightIdentity
  d_RightIdentity_322 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> ([AgdaAny] -> [AgdaAny] -> [AgdaAny]) -> ()
  d_RightIdentity_322 = erased
  -- Data.List.Properties._._.IsMagma
  d_IsMagma_398 a0 a1 a2 = ()
  -- Data.List.Properties._._.IsMonoid
  d_IsMonoid_404 a0 a1 a2 a3 = ()
  -- Data.List.Properties._._.IsSemigroup
  d_IsSemigroup_426 a0 a1 a2 = ()
  -- Data.List.Properties._._.IsMagma.isEquivalence
  d_isEquivalence_1698 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_1698 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isEquivalence_184 (coe v0)
  -- Data.List.Properties._._.IsMagma.∙-cong
  d_'8729''45'cong_1712 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176 ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8729''45'cong_1712 = erased
  -- Data.List.Properties._._.IsMonoid.identity
  d_identity_1808 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_identity_1808 v0
    = coe MAlonzo.Code.Algebra.Structures.d_identity_698 (coe v0)
  -- Data.List.Properties._._.IsMonoid.isSemigroup
  d_isSemigroup_1820 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686 ->
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_isSemigroup_1820 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isSemigroup_696 (coe v0)
  -- Data.List.Properties._._.IsSemigroup.assoc
  d_assoc_2552 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_assoc_2552 = erased
  -- Data.List.Properties._._.IsSemigroup.isMagma
  d_isMagma_2556 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472 ->
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_isMagma_2556 v0
    = coe MAlonzo.Code.Algebra.Structures.d_isMagma_480 (coe v0)
  -- Data.List.Properties._.++-assoc
  d_'43''43''45'assoc_2866 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'assoc_2866 = erased
  -- Data.List.Properties._.++-identityˡ
  d_'43''43''45'identity'737'_2882 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'identity'737'_2882 = erased
  -- Data.List.Properties._.++-identityʳ
  d_'43''43''45'identity'691'_2886 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'identity'691'_2886 = erased
  -- Data.List.Properties._.++-identity
  d_'43''43''45'identity_2894 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'43''43''45'identity_2894 ~v0 ~v1 = du_'43''43''45'identity_2894
  du_'43''43''45'identity_2894 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'43''43''45'identity_2894
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.List.Properties._.++-identityʳ-unique
  d_'43''43''45'identity'691''45'unique_2900 ::
    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_'43''43''45'identity'691''45'unique_2900 = erased
  -- Data.List.Properties._.++-identityˡ-unique
  d_'43''43''45'identity'737''45'unique_2912 ::
    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_'43''43''45'identity'737''45'unique_2912 = erased
  -- Data.List.Properties._.++-cancelˡ
  d_'43''43''45'cancel'737'_2944 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'cancel'737'_2944 = erased
  -- Data.List.Properties._.++-cancelʳ
  d_'43''43''45'cancel'691'_2954 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'cancel'691'_2954 = erased
  -- Data.List.Properties._.++-cancel
  d_'43''43''45'cancel_2982 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'43''43''45'cancel_2982 ~v0 ~v1 = du_'43''43''45'cancel_2982
  du_'43''43''45'cancel_2982 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'43''43''45'cancel_2982
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.List.Properties._.++-conicalˡ
  d_'43''43''45'conical'737'_2988 ::
    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_'43''43''45'conical'737'_2988 = erased
  -- Data.List.Properties._.++-conicalʳ
  d_'43''43''45'conical'691'_2994 ::
    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_'43''43''45'conical'691'_2994 = erased
  -- Data.List.Properties._.++-conical
  d_'43''43''45'conical_2996 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'43''43''45'conical_2996 ~v0 ~v1 = du_'43''43''45'conical_2996
  du_'43''43''45'conical_2996 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'43''43''45'conical_2996
    = coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased
  -- Data.List.Properties._.++-isMagma
  d_'43''43''45'isMagma_2998 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  d_'43''43''45'isMagma_2998 ~v0 ~v1 = du_'43''43''45'isMagma_2998
  du_'43''43''45'isMagma_2998 ::
    MAlonzo.Code.Algebra.Structures.T_IsMagma_176
  du_'43''43''45'isMagma_2998
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMagma'46'constructor_1867
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_isEquivalence_396)
        erased
  -- Data.List.Properties._.++-isSemigroup
  d_'43''43''45'isSemigroup_3000 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  d_'43''43''45'isSemigroup_3000 ~v0 ~v1
    = du_'43''43''45'isSemigroup_3000
  du_'43''43''45'isSemigroup_3000 ::
    MAlonzo.Code.Algebra.Structures.T_IsSemigroup_472
  du_'43''43''45'isSemigroup_3000
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsSemigroup'46'constructor_10417
        (coe du_'43''43''45'isMagma_2998) erased
  -- Data.List.Properties._.++-isMonoid
  d_'43''43''45'isMonoid_3002 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  d_'43''43''45'isMonoid_3002 ~v0 ~v1 = du_'43''43''45'isMonoid_3002
  du_'43''43''45'isMonoid_3002 ::
    MAlonzo.Code.Algebra.Structures.T_IsMonoid_686
  du_'43''43''45'isMonoid_3002
    = coe
        MAlonzo.Code.Algebra.Structures.C_IsMonoid'46'constructor_15873
        (coe du_'43''43''45'isSemigroup_3000)
        (coe du_'43''43''45'identity_2894)
  -- Data.List.Properties._.++-semigroup
  d_'43''43''45'semigroup_3012 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
  d_'43''43''45'semigroup_3012 ~v0 ~v1
    = du_'43''43''45'semigroup_3012
  du_'43''43''45'semigroup_3012 ::
    MAlonzo.Code.Algebra.Bundles.T_Semigroup_536
  du_'43''43''45'semigroup_3012
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Semigroup'46'constructor_9793
        (coe MAlonzo.Code.Data.List.Base.du__'43''43'__32)
        (coe du_'43''43''45'isSemigroup_3000)
  -- Data.List.Properties._.++-monoid
  d_'43''43''45'monoid_3014 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Algebra.Bundles.T_Monoid_882
  d_'43''43''45'monoid_3014 ~v0 ~v1 = du_'43''43''45'monoid_3014
  du_'43''43''45'monoid_3014 ::
    MAlonzo.Code.Algebra.Bundles.T_Monoid_882
  du_'43''43''45'monoid_3014
    = coe
        MAlonzo.Code.Algebra.Bundles.C_Monoid'46'constructor_16157
        (coe MAlonzo.Code.Data.List.Base.du__'43''43'__32)
        (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
        (coe du_'43''43''45'isMonoid_3002)
  -- Data.List.Properties._.length-isMagmaHomomorphism
  d_length'45'isMagmaHomomorphism_3024 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Algebra.Morphism.Structures.T_IsMagmaHomomorphism_176
  d_length'45'isMagmaHomomorphism_3024 ~v0 ~v1
    = du_length'45'isMagmaHomomorphism_3024
  du_length'45'isMagmaHomomorphism_3024 ::
    MAlonzo.Code.Algebra.Morphism.Structures.T_IsMagmaHomomorphism_176
  du_length'45'isMagmaHomomorphism_3024
    = coe
        MAlonzo.Code.Algebra.Morphism.Structures.C_IsMagmaHomomorphism'46'constructor_4629
        (coe
           MAlonzo.Code.Relation.Binary.Morphism.Structures.C_IsRelHomomorphism'46'constructor_587
           erased)
        erased
  -- Data.List.Properties._.length-isMonoidHomomorphism
  d_length'45'isMonoidHomomorphism_3030 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Algebra.Morphism.Structures.T_IsMonoidHomomorphism_350
  d_length'45'isMonoidHomomorphism_3030 ~v0 ~v1
    = du_length'45'isMonoidHomomorphism_3030
  du_length'45'isMonoidHomomorphism_3030 ::
    MAlonzo.Code.Algebra.Morphism.Structures.T_IsMonoidHomomorphism_350
  du_length'45'isMonoidHomomorphism_3030
    = coe
        MAlonzo.Code.Algebra.Morphism.Structures.C_IsMonoidHomomorphism'46'constructor_9411
        (coe du_length'45'isMagmaHomomorphism_3024) erased
  -- Data.List.Properties._.prod
  d_prod_3044 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> [AgdaAny] -> [AgdaAny]
  d_prod_3044 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_prod_3044 v6
  du_prod_3044 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> [AgdaAny] -> [AgdaAny]
  du_prod_3044 v0
    = coe
        MAlonzo.Code.Data.List.Base.du_cartesianProductWith_70 (coe v0)
  -- Data.List.Properties._.cartesianProductWith-zeroˡ
  d_cartesianProductWith'45'zero'737'_3048 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cartesianProductWith'45'zero'737'_3048 = erased
  -- Data.List.Properties._.cartesianProductWith-zeroʳ
  d_cartesianProductWith'45'zero'691'_3052 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cartesianProductWith'45'zero'691'_3052 = erased
  -- Data.List.Properties._.cartesianProductWith-distribʳ-++
  d_cartesianProductWith'45'distrib'691''45''43''43'_3064 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_cartesianProductWith'45'distrib'691''45''43''43'_3064 = erased
  -- Data.List.Properties._.alignWith-cong
  d_alignWith'45'cong_3096 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    (MAlonzo.Code.Data.These.Base.T_These_38 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_alignWith'45'cong_3096 = erased
  -- Data.List.Properties._.length-alignWith
  d_length'45'alignWith_3132 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'alignWith_3132 = erased
  -- Data.List.Properties._.alignWith-map
  d_alignWith'45'map_3154 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_alignWith'45'map_3154 = erased
  -- Data.List.Properties._.map-alignWith
  d_map'45'alignWith_3186 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'alignWith_3186 = erased
  -- Data.List.Properties._.alignWith-flip
  d_alignWith'45'flip_3210 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_alignWith'45'flip_3210 = erased
  -- Data.List.Properties._.alignWith-comm
  d_alignWith'45'comm_3244 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    (MAlonzo.Code.Data.These.Base.T_These_38 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_alignWith'45'comm_3244 = erased
  -- Data.List.Properties.align-map
  d_align'45'map_3260 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_align'45'map_3260 = erased
  -- Data.List.Properties.align-flip
  d_align'45'flip_3274 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_align'45'flip_3274 = erased
  -- Data.List.Properties._.zipWith-cong
  d_zipWith'45'cong_3300 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'cong_3300 = erased
  -- Data.List.Properties._.zipWith-zeroˡ
  d_zipWith'45'zero'737'_3334 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'zero'737'_3334 = erased
  -- Data.List.Properties._.zipWith-zeroʳ
  d_zipWith'45'zero'691'_3342 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'zero'691'_3342 = erased
  -- Data.List.Properties._.length-zipWith
  d_length'45'zipWith_3352 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'zipWith_3352 = erased
  -- Data.List.Properties._.zipWith-map
  d_zipWith'45'map_3382 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'map_3382 = erased
  -- Data.List.Properties._.map-zipWith
  d_map'45'zipWith_3426 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'zipWith_3426 = erased
  -- Data.List.Properties._.zipWith-flip
  d_zipWith'45'flip_3456 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'flip_3456 = erased
  -- Data.List.Properties._.zipWith-comm
  d_zipWith'45'comm_3494 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'comm_3494 = erased
  -- Data.List.Properties.zip-map
  d_zip'45'map_3510 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zip'45'map_3510 = erased
  -- Data.List.Properties.zip-flip
  d_zip'45'flip_3528 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zip'45'flip_3528 = erased
  -- Data.List.Properties.unalignWith-this
  d_unalignWith'45'this_3536 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unalignWith'45'this_3536 = erased
  -- Data.List.Properties.unalignWith-that
  d_unalignWith'45'that_3546 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unalignWith'45'that_3546 = erased
  -- Data.List.Properties._.unalignWith-cong
  d_unalignWith'45'cong_3568 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38) ->
    (AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unalignWith'45'cong_3568 = erased
  -- Data.List.Properties._.unalignWith-map
  d_unalignWith'45'map_3632 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unalignWith'45'map_3632 = erased
  -- Data.List.Properties._.map-unalignWith
  d_map'45'unalignWith_3684 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'unalignWith_3684 = erased
  -- Data.List.Properties._.unalignWith-alignWith
  d_unalignWith'45'alignWith_3748 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Data.These.Base.T_These_38) ->
    (MAlonzo.Code.Data.These.Base.T_These_38 -> AgdaAny) ->
    (MAlonzo.Code.Data.These.Base.T_These_38 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unalignWith'45'alignWith_3748 = erased
  -- Data.List.Properties._.unzipWith-cong
  d_unzipWith'45'cong_3796 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzipWith'45'cong_3796 = erased
  -- Data.List.Properties._.length-unzipWith₁
  d_length'45'unzipWith'8321'_3820 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'unzipWith'8321'_3820 = erased
  -- Data.List.Properties._.length-unzipWith₂
  d_length'45'unzipWith'8322'_3828 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'unzipWith'8322'_3828 = erased
  -- Data.List.Properties._.zipWith-unzipWith
  d_zipWith'45'unzipWith_3836 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'unzipWith_3836 = erased
  -- Data.List.Properties._.unzipWith-zipWith
  d_unzipWith'45'zipWith_3856 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzipWith'45'zipWith_3856 = erased
  -- Data.List.Properties._.unzipWith-map
  d_unzipWith'45'map_3880 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzipWith'45'map_3880 = erased
  -- Data.List.Properties._.map-unzipWith
  d_map'45'unzipWith_3894 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'unzipWith_3894 = erased
  -- Data.List.Properties._.unzipWith-swap
  d_unzipWith'45'swap_3908 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzipWith'45'swap_3908 = erased
  -- Data.List.Properties._.unzipWith-++
  d_unzipWith'45''43''43'_3918 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzipWith'45''43''43'_3918 = erased
  -- Data.List.Properties.unzip-map
  d_unzip'45'map_3932 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzip'45'map_3932 = erased
  -- Data.List.Properties.unzip-swap
  d_unzip'45'swap_3940 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unzip'45'swap_3940 = erased
  -- Data.List.Properties.zip-unzip
  d_zip'45'unzip_3944 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zip'45'unzip_3944 = erased
  -- Data.List.Properties.unzip-zip
  d_unzip'45'zip_3952 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_unzip'45'zip_3952 = erased
  -- Data.List.Properties.foldr-universal
  d_foldr'45'universal_3966 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    ([AgdaAny] -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    (AgdaAny ->
     [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45'universal_3966 = erased
  -- Data.List.Properties.foldr-cong
  d_foldr'45'cong_4004 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45'cong_4004 = erased
  -- Data.List.Properties.foldr-fusion
  d_foldr'45'fusion_4032 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45'fusion_4032 = erased
  -- Data.List.Properties.id-is-foldr
  d_id'45'is'45'foldr_4048 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_id'45'is'45'foldr_4048 = erased
  -- Data.List.Properties.++-is-foldr
  d_'43''43''45'is'45'foldr_4058 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45'is'45'foldr_4058 = erased
  -- Data.List.Properties.foldr-++
  d_foldr'45''43''43'_4080 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45''43''43'_4080 = erased
  -- Data.List.Properties.map-is-foldr
  d_map'45'is'45'foldr_4104 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'is'45'foldr_4104 = erased
  -- Data.List.Properties.foldr-∷ʳ
  d_foldr'45''8759''691'_4126 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45''8759''691'_4126 = erased
  -- Data.List.Properties.foldr-map
  d_foldr'45'map_4152 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45'map_4152 = erased
  -- Data.List.Properties._.foldr-forcesᵇ
  d_foldr'45'forces'7495'_4190 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  d_foldr'45'forces'7495'_4190 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 v8
    = du_foldr'45'forces'7495'_4190 v4 v5 v6 v7 v8
  du_foldr'45'forces'7495'_4190 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny -> MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  du_foldr'45'forces'7495'_4190 v0 v1 v2 v3 v4
    = case coe v3 of
        [] -> coe MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50
        (:) v5 v6
          -> coe
               MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
               (MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                  (coe
                     v1 v5
                     (coe
                        MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                        (coe v6))
                     v4))
               (coe
                  du_foldr'45'forces'7495'_4190 (coe v0) (coe v1) (coe v2) (coe v6)
                  (coe
                     MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                     (coe
                        v1 v5
                        (coe
                           MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                           (coe v6))
                        v4)))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.foldr-preservesᵇ
  d_foldr'45'preserves'7495'_4212 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
  d_foldr'45'preserves'7495'_4212 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 v8 v9
    = du_foldr'45'preserves'7495'_4212 v4 v5 v6 v7 v8 v9
  du_foldr'45'preserves'7495'_4212 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 -> AgdaAny
  du_foldr'45'preserves'7495'_4212 v0 v1 v2 v3 v4 v5
    = case coe v5 of
        MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50 -> coe v4
        MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 v8 v9
          -> case coe v3 of
               (:) v10 v11
                 -> coe
                      v1 v10
                      (coe
                         MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                         (coe v11))
                      v8
                      (coe
                         du_foldr'45'preserves'7495'_4212 (coe v0) (coe v1) (coe v2)
                         (coe v11) (coe v4) (coe v9))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.foldr-preservesʳ
  d_foldr'45'preserves'691'_4232 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
  d_foldr'45'preserves'691'_4232 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 v8
    = du_foldr'45'preserves'691'_4232 v4 v5 v6 v7 v8
  du_foldr'45'preserves'691'_4232 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny -> AgdaAny -> [AgdaAny] -> AgdaAny
  du_foldr'45'preserves'691'_4232 v0 v1 v2 v3 v4
    = case coe v4 of
        [] -> coe v3
        (:) v5 v6
          -> coe
               v1 v5
               (coe
                  MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                  (coe v6))
               (coe
                  du_foldr'45'preserves'691'_4232 (coe v0) (coe v1) (coe v2) (coe v3)
                  (coe v6))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.foldr-preservesᵒ
  d_foldr'45'preserves'7506'_4252 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
  d_foldr'45'preserves'7506'_4252 ~v0 ~v1 ~v2 ~v3 v4 v5 v6 v7 v8
    = du_foldr'45'preserves'7506'_4252 v4 v5 v6 v7 v8
  du_foldr'45'preserves'7506'_4252 ::
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Data.Sum.Base.T__'8846'__30 -> AgdaAny
  du_foldr'45'preserves'7506'_4252 v0 v1 v2 v3 v4
    = case coe v3 of
        []
          -> case coe v4 of
               MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v5 -> coe v5
               _                                            -> MAlonzo.RTE.mazUnreachableError
        (:) v5 v6
          -> case coe v4 of
               MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 v7
                 -> coe
                      v1 v5
                      (coe
                         MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                         (coe v6))
                      (coe
                         MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                         (coe
                            du_foldr'45'preserves'7506'_4252 (coe v0) (coe v1) (coe v2)
                            (coe v6) (coe v4)))
               MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 v7
                 -> case coe v7 of
                      MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v10
                        -> coe
                             v1 v5
                             (coe
                                MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                                (coe v6))
                             (coe MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 (coe v10))
                      MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v10
                        -> coe
                             v1 v5
                             (coe
                                MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v0) (coe v2)
                                (coe v6))
                             (coe
                                MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42
                                (coe
                                   du_foldr'45'preserves'7506'_4252 (coe v0) (coe v1) (coe v2)
                                   (coe v6)
                                   (coe MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 (coe v10))))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.foldl-cong
  d_foldl'45'cong_4300 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldl'45'cong_4300 = erased
  -- Data.List.Properties.foldl-++
  d_foldl'45''43''43'_4326 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldl'45''43''43'_4326 = erased
  -- Data.List.Properties.foldl-∷ʳ
  d_foldl'45''8759''691'_4352 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldl'45''8759''691'_4352 = erased
  -- Data.List.Properties.foldl-map
  d_foldl'45'map_4378 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldl'45'map_4378 = erased
  -- Data.List.Properties.concat-map
  d_concat'45'map_4398 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [[AgdaAny]] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concat'45'map_4398 = erased
  -- Data.List.Properties.concat-++
  d_concat'45''43''43'_4420 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [[AgdaAny]] ->
    [[AgdaAny]] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concat'45''43''43'_4420 = erased
  -- Data.List.Properties.concat-concat
  d_concat'45'concat_4438 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [[[AgdaAny]]] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concat'45'concat_4438 = erased
  -- Data.List.Properties.concat-[-]
  d_concat'45''91''45''93'_4446 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concat'45''91''45''93'_4446 = erased
  -- Data.List.Properties.concatMap-cong
  d_concatMap'45'cong_4458 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> [AgdaAny]) ->
    (AgdaAny -> [AgdaAny]) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concatMap'45'cong_4458 = erased
  -- Data.List.Properties.concatMap-pure
  d_concatMap'45'pure_4464 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concatMap'45'pure_4464 = erased
  -- Data.List.Properties.concatMap-map
  d_concatMap'45'map_4472 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> [AgdaAny]) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_concatMap'45'map_4472 = erased
  -- Data.List.Properties.map-concatMap
  d_map'45'concatMap_4484 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> [AgdaAny]) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'concatMap_4484 = erased
  -- Data.List.Properties.catMaybes-concatMap
  d_catMaybes'45'concatMap_4492 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [Maybe AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_catMaybes'45'concatMap_4492 = erased
  -- Data.List.Properties.length-catMaybes
  d_length'45'catMaybes_4504 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [Maybe AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_length'45'catMaybes_4504 ~v0 ~v1 v2
    = du_length'45'catMaybes_4504 v2
  du_length'45'catMaybes_4504 ::
    [Maybe AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_length'45'catMaybes_4504 v0
    = case coe v0 of
        []
          -> coe
               MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776
               (coe
                  MAlonzo.Code.Data.List.Base.du_length_284
                  (coe MAlonzo.Code.Data.List.Base.du_catMaybes_256 v0))
        (:) v1 v2
          -> case coe v1 of
               MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v3
                 -> coe
                      MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                      (coe du_length'45'catMaybes_4504 (coe v2))
               MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                 -> coe du_length'45'catMaybes_4504 (coe v2)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.catMaybes-++
  d_catMaybes'45''43''43'_4514 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [Maybe AgdaAny] ->
    [Maybe AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_catMaybes'45''43''43'_4514 = erased
  -- Data.List.Properties.map-catMaybes
  d_map'45'catMaybes_4530 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [Maybe AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'catMaybes_4530 = erased
  -- Data.List.Properties.Any-catMaybes⁺
  d_Any'45'catMaybes'8314'_4548 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    [Maybe AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
  d_Any'45'catMaybes'8314'_4548 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_Any'45'catMaybes'8314'_4548 v4 v5
  du_Any'45'catMaybes'8314'_4548 ::
    [Maybe AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
  du_Any'45'catMaybes'8314'_4548 v0 v1
    = case coe v0 of
        (:) v2 v3
          -> case coe v2 of
               MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 v4
                 -> case coe v1 of
                      MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v7
                        -> case coe v7 of
                             MAlonzo.Code.Data.Maybe.Relation.Unary.Any.C_just_30 v9
                               -> coe MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v9
                             _ -> MAlonzo.RTE.mazUnreachableError
                      MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v7
                        -> coe
                             MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                             (coe du_Any'45'catMaybes'8314'_4548 (coe v3) (coe v7))
                      _ -> MAlonzo.RTE.mazUnreachableError
               MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
                 -> case coe v1 of
                      MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v6
                        -> coe du_Any'45'catMaybes'8314'_4548 (coe v3) (coe v6)
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.mapMaybe-cong
  d_mapMaybe'45'cong_4570 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    (AgdaAny -> Maybe AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'cong_4570 = erased
  -- Data.List.Properties.mapMaybe-just
  d_mapMaybe'45'just_4576 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'just_4576 = erased
  -- Data.List.Properties.mapMaybe-nothing
  d_mapMaybe'45'nothing_4588 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'nothing_4588 = erased
  -- Data.List.Properties._.mapMaybe-concatMap
  d_mapMaybe'45'concatMap_4604 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'concatMap_4604 = erased
  -- Data.List.Properties._.length-mapMaybe
  d_length'45'mapMaybe_4610 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_length'45'mapMaybe_4610 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_length'45'mapMaybe_4610 v4 v5
  du_length'45'mapMaybe_4610 ::
    (AgdaAny -> Maybe AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_length'45'mapMaybe_4610 v0 v1
    = coe
        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
           (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
           (\ v2 v3 v4 ->
              coe MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 v4))
        (coe
           MAlonzo.Code.Data.List.Base.du_length_284
           (coe
              MAlonzo.Code.Data.List.Base.du_mapMaybe_258 (coe v0) (coe v1)))
        (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
        (coe
           MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
           (coe
              MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
              (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
              (\ v2 v3 v4 v5 v6 ->
                 coe
                   MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 v5
                   v6))
           (coe
              MAlonzo.Code.Data.List.Base.du_length_284
              (coe
                 MAlonzo.Code.Data.List.Base.du_mapMaybe_258 (coe v0) (coe v1)))
           (coe
              MAlonzo.Code.Data.List.Base.du_length_284
              (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe v0) (coe v1)))
           (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
           (coe
              MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
              (coe
                 MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
                 (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
                 (\ v2 v3 v4 v5 v6 ->
                    coe
                      MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 v5
                      v6))
              (coe
                 MAlonzo.Code.Data.List.Base.du_length_284
                 (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe v0) (coe v1)))
              (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
              (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
              (coe
                 MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                 (coe
                    MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                    (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                 (coe MAlonzo.Code.Data.List.Base.du_length_284 v1))
              (coe
                 MAlonzo.Code.Data.Nat.Properties.du_'8804''45'reflexive_2772
                 (coe
                    MAlonzo.Code.Data.List.Base.du_length_284
                    (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe v0) (coe v1)))))
           (coe
              du_length'45'catMaybes_4504
              (coe MAlonzo.Code.Data.List.Base.du_map_22 (coe v0) (coe v1))))
  -- Data.List.Properties._.mapMaybe-++
  d_mapMaybe'45''43''43'_4622 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45''43''43'_4622 = erased
  -- Data.List.Properties._.mapMaybe-map
  d_mapMaybe'45'map_4642 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'map_4642 = erased
  -- Data.List.Properties._.map-mapMaybe
  d_map'45'mapMaybe_4658 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> Maybe AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'mapMaybe_4658 = erased
  -- Data.List.Properties._.mapMaybe-map-retract
  d_mapMaybe'45'map'45'retract_4674 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'map'45'retract_4674 = erased
  -- Data.List.Properties._.mapMaybe-map-none
  d_mapMaybe'45'map'45'none_4694 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> Maybe AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybe'45'map'45'none_4694 = erased
  -- Data.List.Properties.mapMaybeIsInj₁∘mapInj₁
  d_mapMaybeIsInj'8321''8728'mapInj'8321'_4702 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybeIsInj'8321''8728'mapInj'8321'_4702 = erased
  -- Data.List.Properties.mapMaybeIsInj₁∘mapInj₂
  d_mapMaybeIsInj'8321''8728'mapInj'8322'_4708 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybeIsInj'8321''8728'mapInj'8322'_4708 = erased
  -- Data.List.Properties.mapMaybeIsInj₂∘mapInj₂
  d_mapMaybeIsInj'8322''8728'mapInj'8322'_4714 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybeIsInj'8322''8728'mapInj'8322'_4714 = erased
  -- Data.List.Properties.mapMaybeIsInj₂∘mapInj₁
  d_mapMaybeIsInj'8322''8728'mapInj'8321'_4720 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_mapMaybeIsInj'8322''8728'mapInj'8321'_4720 = erased
  -- Data.List.Properties.sum-++
  d_sum'45''43''43'_4728 ::
    [Integer] ->
    [Integer] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_sum'45''43''43'_4728 = erased
  -- Data.List.Properties.∈⇒∣product
  d_'8712''8658''8739'product_4744 ::
    Integer ->
    [Integer] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
  d_'8712''8658''8739'product_4744 ~v0 v1 v2
    = du_'8712''8658''8739'product_4744 v1 v2
  du_'8712''8658''8739'product_4744 ::
    [Integer] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Divisibility.Core.T__'8739'__20
  du_'8712''8658''8739'product_4744 v0 v1
    = case coe v0 of
        (:) v2 v3
          -> case coe v1 of
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v6
                 -> coe
                      MAlonzo.Code.Data.Nat.Divisibility.Core.C_divides_34
                      (coe MAlonzo.Code.Data.List.Base.d_product_282 v3)
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v6
                 -> coe
                      MAlonzo.Code.Data.Nat.Divisibility.du_'8739'n'8658''8739'm'42'n_374
                      v2 (coe du_'8712''8658''8739'product_4744 (coe v3) (coe v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.length-applyUpTo
  d_length'45'applyUpTo_4762 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'applyUpTo_4762 = erased
  -- Data.List.Properties.lookup-applyUpTo
  d_lookup'45'applyUpTo_4776 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'applyUpTo_4776 = erased
  -- Data.List.Properties.applyUpTo-∷ʳ
  d_applyUpTo'45''8759''691'_4792 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_applyUpTo'45''8759''691'_4792 = erased
  -- Data.List.Properties._.length-applyDownFrom
  d_length'45'applyDownFrom_4812 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'applyDownFrom_4812 = erased
  -- Data.List.Properties._.lookup-applyDownFrom
  d_lookup'45'applyDownFrom_4820 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'applyDownFrom_4820 = erased
  -- Data.List.Properties._.applyDownFrom-∷ʳ
  d_applyDownFrom'45''8759''691'_4830 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_applyDownFrom'45''8759''691'_4830 = erased
  -- Data.List.Properties.length-upTo
  d_length'45'upTo_4838 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'upTo_4838 = erased
  -- Data.List.Properties.lookup-upTo
  d_lookup'45'upTo_4844 ::
    Integer ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'upTo_4844 = erased
  -- Data.List.Properties.upTo-∷ʳ
  d_upTo'45''8759''691'_4848 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_upTo'45''8759''691'_4848 = erased
  -- Data.List.Properties.length-downFrom
  d_length'45'downFrom_4852 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'downFrom_4852 = erased
  -- Data.List.Properties.lookup-downFrom
  d_lookup'45'downFrom_4858 ::
    Integer ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'downFrom_4858 = erased
  -- Data.List.Properties.downFrom-∷ʳ
  d_downFrom'45''8759''691'_4862 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_downFrom'45''8759''691'_4862 = erased
  -- Data.List.Properties.tabulate-cong
  d_tabulate'45'cong_4870 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_tabulate'45'cong_4870 = erased
  -- Data.List.Properties.tabulate-lookup
  d_tabulate'45'lookup_4880 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_tabulate'45'lookup_4880 = erased
  -- Data.List.Properties.length-tabulate
  d_length'45'tabulate_4892 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'tabulate_4892 = erased
  -- Data.List.Properties.lookup-tabulate
  d_lookup'45'tabulate_4910 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'tabulate_4910 = erased
  -- Data.List.Properties.map-tabulate
  d_map'45'tabulate_4924 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'tabulate_4924 = erased
  -- Data.List.Properties.length-%=
  d_length'45''37''61'_4944 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45''37''61'_4944 = erased
  -- Data.List.Properties.length-∷=
  d_length'45''8759''61'_4966 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45''8759''61'_4966 = erased
  -- Data.List.Properties.map-∷=
  d_map'45''8759''61'_4984 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    AgdaAny ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''8759''61'_4984 = erased
  -- Data.List.Properties.length-insertAt
  d_length'45'insertAt_5012 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'insertAt_5012 = erased
  -- Data.List.Properties.length-removeAt
  d_length'45'removeAt_5030 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'removeAt_5030 = erased
  -- Data.List.Properties.length-removeAt′
  d_length'45'removeAt'8242'_5046 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'removeAt'8242'_5046 = erased
  -- Data.List.Properties.map-removeAt
  d_map'45'removeAt_5064 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'removeAt_5064 = erased
  -- Data.List.Properties.removeAt-insertAt
  d_removeAt'45'insertAt_5088 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_removeAt'45'insertAt_5088 = erased
  -- Data.List.Properties.insertAt-removeAt
  d_insertAt'45'removeAt_5108 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_insertAt'45'removeAt_5108 = erased
  -- Data.List.Properties.length-take
  d_length'45'take_5126 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'take_5126 = erased
  -- Data.List.Properties.take-map
  d_take'45'map_5144 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'map_5144 = erased
  -- Data.List.Properties.take-suc
  d_take'45'suc_5164 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'suc_5164 = erased
  -- Data.List.Properties.take-suc-tabulate
  d_take'45'suc'45'tabulate_5186 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'suc'45'tabulate_5186 = erased
  -- Data.List.Properties.take-all
  d_take'45'all_5204 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'all_5204 = erased
  -- Data.List.Properties.take-[]
  d_take'45''91''93'_5218 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45''91''93'_5218 = erased
  -- Data.List.Properties.take-take
  d_take'45'take_5228 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'take_5228 = erased
  -- Data.List.Properties.take-drop
  d_take'45'drop_5258 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'45'drop_5258 = erased
  -- Data.List.Properties.length-drop
  d_length'45'drop_5280 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'drop_5280 = erased
  -- Data.List.Properties.drop-map
  d_drop'45'map_5298 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45'map_5298 = erased
  -- Data.List.Properties.drop-[]
  d_drop'45''91''93'_5312 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45''91''93'_5312 = erased
  -- Data.List.Properties.take++drop≡id
  d_take'43''43'drop'8801'id_5320 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'43''43'drop'8801'id_5320 = erased
  -- Data.List.Properties.drop-take-suc
  d_drop'45'take'45'suc_5340 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45'take'45'suc_5340 = erased
  -- Data.List.Properties.drop-take-suc-tabulate
  d_drop'45'take'45'suc'45'tabulate_5360 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45'take'45'suc'45'tabulate_5360 = erased
  -- Data.List.Properties.drop-drop
  d_drop'45'drop_5380 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45'drop_5380 = erased
  -- Data.List.Properties.drop-all
  d_drop'45'all_5402 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_drop'45'all_5402 = erased
  -- Data.List.Properties.length-replicate
  d_length'45'replicate_5418 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'replicate_5418 = erased
  -- Data.List.Properties.lookup-replicate
  d_lookup'45'replicate_5428 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    AgdaAny ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'replicate_5428 = erased
  -- Data.List.Properties.map-replicate
  d_map'45'replicate_5446 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Integer ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'replicate_5446 = erased
  -- Data.List.Properties.zipWith-replicate
  d_zipWith'45'replicate_5468 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'replicate_5468 = erased
  -- Data.List.Properties.length-iterate
  d_length'45'iterate_5492 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'iterate_5492 = erased
  -- Data.List.Properties.iterate-id
  d_iterate'45'id_5508 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_iterate'45'id_5508 = erased
  -- Data.List.Properties.lookup-iterate
  d_lookup'45'iterate_5526 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    AgdaAny ->
    Integer ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_lookup'45'iterate_5526 = erased
  -- Data.List.Properties.splitAt-defn
  d_splitAt'45'defn_5544 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_splitAt'45'defn_5544 = erased
  -- Data.List.Properties._.splitAt-map
  d_splitAt'45'map_5570 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_splitAt'45'map_5570 = erased
  -- Data.List.Properties._.takeWhile++dropWhile
  d_takeWhile'43''43'dropWhile_5598 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_takeWhile'43''43'dropWhile_5598 = erased
  -- Data.List.Properties._.span-defn
  d_span'45'defn_5618 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_span'45'defn_5618 = erased
  -- Data.List.Properties._.length-filter
  d_length'45'filter_5652 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_length'45'filter_5652 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_length'45'filter_5652 v4 v5
  du_length'45'filter_5652 ::
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_length'45'filter_5652 v0 v1
    = case coe v1 of
        [] -> coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
        (:) v2 v3
          -> let v4 = coe du_length'45'filter_5652 (coe v0) (coe v3) in
             coe
               (let v5
                      = MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                          (coe v0 v2) in
                coe
                  (if coe v5
                     then coe MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 v4
                     else coe v4))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.filter-all
  d_filter'45'all_5678 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'all_5678 = erased
  -- Data.List.Properties._.filter-notAll
  d_filter'45'notAll_5714 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_filter'45'notAll_5714 ~v0 ~v1 ~v2 ~v3 v4 v5 v6
    = du_filter'45'notAll_5714 v4 v5 v6
  du_filter'45'notAll_5714 ::
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_filter'45'notAll_5714 v0 v1 v2
    = case coe v1 of
        (:) v3 v4
          -> case coe v2 of
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v7
                 -> let v8 = coe v0 v3 in
                    coe
                      (case coe v8 of
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10
                           -> if coe v9
                                then coe
                                       seq (coe v10)
                                       (coe
                                          MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                          erased)
                                else coe
                                       MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                                       (coe du_length'45'filter_5652 (coe v0) (coe v4))
                         _ -> MAlonzo.RTE.mazUnreachableError)
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v7
                 -> let v8
                          = coe du_filter'45'notAll_5714 (coe v0) (coe v4) (coe v7) in
                    coe
                      (let v9
                             = MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                                 (coe v0 v3) in
                       coe
                         (if coe v9
                            then coe MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 v8
                            else coe v8))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.filter-some
  d_filter'45'some_5770 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_filter'45'some_5770 ~v0 ~v1 ~v2 ~v3 v4 v5 v6
    = du_filter'45'some_5770 v4 v5 v6
  du_filter'45'some_5770 ::
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_filter'45'some_5770 v0 v1 v2
    = case coe v1 of
        (:) v3 v4
          -> case coe v2 of
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v7
                 -> let v8 = coe v0 v3 in
                    coe
                      (case coe v8 of
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v9 v10
                           -> if coe v9
                                then coe
                                       MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                                       (coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26)
                                else coe
                                       seq (coe v10)
                                       (coe
                                          MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                          erased)
                         _ -> MAlonzo.RTE.mazUnreachableError)
               MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v7
                 -> let v8
                          = MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                              (coe v0 v3) in
                    coe
                      (coe
                         seq (coe v8)
                         (coe du_filter'45'some_5770 (coe v0) (coe v4) (coe v7)))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.filter-none
  d_filter'45'none_5820 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'none_5820 = erased
  -- Data.List.Properties._.filter-complete
  d_filter'45'complete_5854 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'complete_5854 = erased
  -- Data.List.Properties._.filter-accept
  d_filter'45'accept_5886 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'accept_5886 = erased
  -- Data.List.Properties._.filter-reject
  d_filter'45'reject_5910 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    [AgdaAny] ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'reject_5910 = erased
  -- Data.List.Properties._.filter-idem
  d_filter'45'idem_5930 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45'idem_5930 = erased
  -- Data.List.Properties._.filter-++
  d_filter'45''43''43'_5960 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_filter'45''43''43'_5960 = erased
  -- Data.List.Properties._.length-derun
  d_length'45'derun_6008 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_length'45'derun_6008 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_length'45'derun_6008 v4 v5
  du_length'45'derun_6008 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_length'45'derun_6008 v0 v1
    = case coe v1 of
        []
          -> coe
               MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776
               (coe
                  MAlonzo.Code.Data.List.Base.du_length_284
                  (coe MAlonzo.Code.Data.List.Base.du_derun_852 (coe v0) (coe v1)))
        (:) v2 v3
          -> case coe v3 of
               []
                 -> coe
                      MAlonzo.Code.Data.Nat.Properties.d_'8804''45'refl_2776
                      (coe
                         MAlonzo.Code.Data.List.Base.du_length_284
                         (coe MAlonzo.Code.Data.List.Base.du_derun_852 (coe v0) (coe v1)))
               (:) v4 v5
                 -> let v6 = coe du_length'45'derun_6008 (coe v0) (coe v3) in
                    coe
                      (let v7
                             = MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                                 (coe v0 v2 v4) in
                       coe
                         (if coe v7
                            then coe v6
                            else coe MAlonzo.Code.Data.Nat.Base.C_s'8804's_34 v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._.length-deduplicate
  d_length'45'deduplicate_6042 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  d_length'45'deduplicate_6042 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_length'45'deduplicate_6042 v4 v5
  du_length'45'deduplicate_6042 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Data.Nat.Base.T__'8804'__22
  du_length'45'deduplicate_6042 v0 v1
    = case coe v1 of
        [] -> coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26
        (:) v2 v3
          -> coe
               MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_begin__46
               (coe
                  MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_start_96
                  (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
                  (\ v4 v5 v6 ->
                     coe MAlonzo.Code.Data.Nat.Properties.du_'60''8658''8804'_2854 v6))
               (coe
                  MAlonzo.Code.Data.List.Base.du_length_284
                  (coe
                     MAlonzo.Code.Data.List.Base.du_deduplicate_898 (coe v0) (coe v1)))
               (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
               (coe
                  MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
                  (coe
                     MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
                     (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
                     (\ v4 v5 v6 v7 v8 ->
                        coe
                          MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 v7
                          v8))
                  (addInt
                     (coe (1 :: Integer))
                     (coe
                        MAlonzo.Code.Data.List.Base.du_length_284
                        (coe
                           MAlonzo.Code.Data.List.Base.du_filter_664
                           (coe
                              (\ v4 ->
                                 coe
                                   MAlonzo.Code.Relation.Nullary.Decidable.Core.du_'172''63'_70
                                   (coe v0 v2 v4)))
                           (coe du_r_6052 (coe v0) (coe v3)))))
                  (addInt
                     (coe (1 :: Integer))
                     (coe
                        MAlonzo.Code.Data.List.Base.du_length_284
                        (coe du_r_6052 (coe v0) (coe v3))))
                  (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
                  (coe
                     MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du_step'45''8804'_308
                     (coe
                        MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_'8804''45'go_138
                        (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810)
                        (\ v4 v5 v6 v7 v8 ->
                           coe
                             MAlonzo.Code.Data.Nat.Properties.du_'8804''45''60''45'trans_2986 v7
                             v8))
                     (addInt
                        (coe (1 :: Integer))
                        (coe
                           MAlonzo.Code.Data.List.Base.du_length_284
                           (coe du_r_6052 (coe v0) (coe v3))))
                     (addInt
                        (coe (1 :: Integer))
                        (coe MAlonzo.Code.Data.List.Base.du_length_284 v3))
                     (coe MAlonzo.Code.Data.List.Base.du_length_284 v1)
                     (coe
                        MAlonzo.Code.Relation.Binary.Reasoning.Syntax.du__'8718'_492
                        (coe
                           MAlonzo.Code.Relation.Binary.Reasoning.Base.Triple.du_stop_166
                           (coe MAlonzo.Code.Data.Nat.Properties.d_'8804''45'isPreorder_2810))
                        (coe
                           addInt (coe (1 :: Integer))
                           (coe MAlonzo.Code.Data.List.Base.du_length_284 v3)))
                     (coe
                        MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                        (coe du_length'45'deduplicate_6042 (coe v0) (coe v3))))
                  (coe
                     MAlonzo.Code.Data.Nat.Base.C_s'8804's_34
                     (coe
                        du_length'45'filter_5652
                        (coe
                           (\ v4 ->
                              coe
                                MAlonzo.Code.Relation.Nullary.Decidable.Core.du_'172''63'_70
                                (coe v0 v2 v4)))
                        (coe du_r_6052 (coe v0) (coe v3)))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties._._.r
  d_r_6052 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny -> [AgdaAny] -> [AgdaAny]
  d_r_6052 ~v0 ~v1 ~v2 ~v3 v4 ~v5 v6 = du_r_6052 v4 v6
  du_r_6052 ::
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> [AgdaAny]
  du_r_6052 v0 v1
    = coe
        MAlonzo.Code.Data.List.Base.du_deduplicate_898 (coe v0) (coe v1)
  -- Data.List.Properties._.derun-reject
  d_derun'45'reject_6060 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_derun'45'reject_6060 = erased
  -- Data.List.Properties._.derun-accept
  d_derun'45'accept_6098 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_derun'45'accept_6098 = erased
  -- Data.List.Properties._.partition-defn
  d_partition'45'defn_6142 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_partition'45'defn_6142 = erased
  -- Data.List.Properties._.length-partition
  d_length'45'partition_6176 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_length'45'partition_6176 ~v0 ~v1 ~v2 ~v3 v4 v5
    = du_length'45'partition_6176 v4 v5
  du_length'45'partition_6176 ::
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_length'45'partition_6176 v0 v1
    = case coe v1 of
        []
          -> coe
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
               (coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26)
               (coe MAlonzo.Code.Data.Nat.Base.C_z'8804'n_26)
        (:) v2 v3
          -> let v4 = coe du_length'45'partition_6176 (coe v0) (coe v3) in
             coe
               (let v5
                      = MAlonzo.Code.Relation.Nullary.Decidable.Core.d_does_28
                          (coe v0 v2) in
                coe
                  (if coe v5
                     then coe
                            MAlonzo.Code.Data.Product.Base.du_map_128
                            (coe MAlonzo.Code.Data.Nat.Base.C_s'8804's_34)
                            (coe (\ v6 v7 -> v7)) (coe v4)
                     else coe
                            MAlonzo.Code.Data.Product.Base.du_map_128 (coe (\ v6 -> v6))
                            (coe (\ v6 -> coe MAlonzo.Code.Data.Nat.Base.C_s'8804's_34))
                            (coe v4)))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.ʳ++-defn
  d_'691''43''43''45'defn_6204 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'691''43''43''45'defn_6204 = erased
  -- Data.List.Properties.++-ʳ++
  d_'43''43''45''691''43''43'_6220 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'43''43''45''691''43''43'_6220 = erased
  -- Data.List.Properties.ʳ++-ʳ++
  d_'691''43''43''45''691''43''43'_6236 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'691''43''43''45''691''43''43'_6236 = erased
  -- Data.List.Properties.length-ʳ++
  d_length'45''691''43''43'_6250 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45''691''43''43'_6250 = erased
  -- Data.List.Properties.map-ʳ++
  d_map'45''691''43''43'_6264 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''691''43''43'_6264 = erased
  -- Data.List.Properties.foldr-ʳ++
  d_foldr'45''691''43''43'_6284 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'45''691''43''43'_6284 = erased
  -- Data.List.Properties.foldl-ʳ++
  d_foldl'45''691''43''43'_6308 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldl'45''691''43''43'_6308 = erased
  -- Data.List.Properties.unfold-reverse
  d_unfold'45'reverse_6328 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_unfold'45'reverse_6328 = erased
  -- Data.List.Properties.reverse-++
  d_reverse'45''43''43'_6338 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45''43''43'_6338 = erased
  -- Data.List.Properties.reverse-selfInverse
  d_reverse'45'selfInverse_6344 ::
    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_reverse'45'selfInverse_6344 = erased
  -- Data.List.Properties.reverse-involutive
  d_reverse'45'involutive_6354 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'involutive_6354 = erased
  -- Data.List.Properties.reverse-injective
  d_reverse'45'injective_6356 ::
    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_reverse'45'injective_6356 = erased
  -- Data.List.Properties.length-reverse
  d_length'45'reverse_6360 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45'reverse_6360 = erased
  -- Data.List.Properties.reverse-map
  d_reverse'45'map_6366 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'map_6366 = erased
  -- Data.List.Properties.reverse-foldr
  d_reverse'45'foldr_6376 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'foldr_6376 = erased
  -- Data.List.Properties.reverse-foldl
  d_reverse'45'foldl_6390 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'foldl_6390 = erased
  -- Data.List.Properties.reverse-applyUpTo
  d_reverse'45'applyUpTo_6402 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'applyUpTo_6402 = erased
  -- Data.List.Properties.reverse-upTo
  d_reverse'45'upTo_6414 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'upTo_6414 = erased
  -- Data.List.Properties.reverse-applyDownFrom
  d_reverse'45'applyDownFrom_6420 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (Integer -> AgdaAny) ->
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'applyDownFrom_6420 = erased
  -- Data.List.Properties.reverse-downFrom
  d_reverse'45'downFrom_6432 ::
    Integer -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'downFrom_6432 = erased
  -- Data.List.Properties.∷ʳ-injective
  d_'8759''691''45'injective_6438 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'8759''691''45'injective_6438 ~v0 ~v1 ~v2 ~v3 v4 v5 ~v6
    = du_'8759''691''45'injective_6438 v4 v5
  du_'8759''691''45'injective_6438 ::
    [AgdaAny] -> [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'8759''691''45'injective_6438 v0 v1
    = case coe v0 of
        []
          -> coe
               seq (coe v1)
               (coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased erased)
        (:) v2 v3
          -> case coe v1 of
               (:) v4 v5
                 -> let v6 = coe du_'8759''45'injective_46 in
                    coe
                      (coe
                         seq (coe v6)
                         (coe
                            MAlonzo.Code.Data.Product.Base.du_map_128 erased
                            (coe (\ v7 v8 -> v8))
                            (coe du_'8759''691''45'injective_6438 (coe v3) (coe v5))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Properties.∷ʳ-injectiveˡ
  d_'8759''691''45'injective'737'_6462 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8759''691''45'injective'737'_6462 = erased
  -- Data.List.Properties.∷ʳ-injectiveʳ
  d_'8759''691''45'injective'691'_6474 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    AgdaAny ->
    AgdaAny ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8759''691''45'injective'691'_6474 = erased
  -- Data.List.Properties.∷ʳ-++
  d_'8759''691''45''43''43'_6488 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'8759''691''45''43''43'_6488 = erased
  -- Data.List.Properties._.uncons-map
  d_uncons'45'map_6506 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_uncons'45'map_6506 = erased
  -- Data.List.Properties._.head-map
  d_head'45'map_6522 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_head'45'map_6522 = erased
  -- Data.List.Properties._.last-map
  d_last'45'map_6534 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_last'45'map_6534 = erased
  -- Data.List.Properties._.tail-map
  d_tail'45'map_6552 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_tail'45'map_6552 = erased
  -- Data.List.Properties.map-id₂
  d_map'45'id'8322'_6558 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'id'8322'_6558 = erased
  -- Data.List.Properties.map-cong₂
  d_map'45'cong'8322'_6560 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'cong'8322'_6560 = erased
  -- Data.List.Properties.map-compose
  d_map'45'compose_6562 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45'compose_6562 = erased
  -- Data.List.Properties.map-++-commute
  d_map'45''43''43''45'commute_6564 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''43''43''45'commute_6564 = erased
  -- Data.List.Properties.sum-++-commute
  d_sum'45''43''43''45'commute_6566 ::
    [Integer] ->
    [Integer] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_sum'45''43''43''45'commute_6566 = erased
  -- Data.List.Properties.reverse-map-commute
  d_reverse'45'map'45'commute_6568 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45'map'45'commute_6568 = erased
  -- Data.List.Properties.reverse-++-commute
  d_reverse'45''43''43''45'commute_6570 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_reverse'45''43''43''45'commute_6570 = erased
  -- Data.List.Properties.zipWith-identityˡ
  d_zipWith'45'identity'737'_6572 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'identity'737'_6572 = erased
  -- Data.List.Properties.zipWith-identityʳ
  d_zipWith'45'identity'691'_6574 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_zipWith'45'identity'691'_6574 = erased
  -- Data.List.Properties.ʳ++-++
  d_'691''43''43''45''43''43'_6576 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_'691''43''43''45''43''43'_6576 = erased
  -- Data.List.Properties.take++drop
  d_take'43''43'drop_6578 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    Integer ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_take'43''43'drop_6578 = erased
  -- Data.List.Properties.length-─
  d_length'45''9472'_6580 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_length'45''9472'_6580 = erased
  -- Data.List.Properties.map-─
  d_map'45''9472'_6582 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_map'45''9472'_6582 = erased
  -- Data.List.Properties.scanr-defn
  d_scanr'45'defn_6588 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_scanr'45'defn_6588 = erased
  -- Data.List.Properties.scanl-defn
  d_scanl'45'defn_6628 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    [AgdaAny] -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_scanl'45'defn_6628 = erased
  