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.Relation.Binary.Pointwise where
  
  import Data.Text qualified
  import MAlonzo.Code.Agda.Builtin.Equality qualified
  import MAlonzo.Code.Agda.Builtin.Sigma qualified
  import MAlonzo.Code.Agda.Primitive qualified
  import MAlonzo.Code.Data.Fin.Base qualified
  import MAlonzo.Code.Data.List.Base qualified
  import MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base qualified
  import MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties qualified
  import MAlonzo.Code.Data.List.Relation.Unary.All qualified
  import MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core qualified
  import MAlonzo.Code.Data.List.Relation.Unary.Any qualified
  import MAlonzo.Code.Function.Bundles qualified
  import MAlonzo.Code.Relation.Binary.Bundles 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.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.Relation.Binary.Pointwise.isEquivalence
  d_isEquivalence_56 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_isEquivalence_56 ~v0 ~v1 ~v2 ~v3 v4 = du_isEquivalence_56 v4
  du_isEquivalence_56 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_isEquivalence_56 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsEquivalence'46'constructor_745
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_refl_30
           (coe MAlonzo.Code.Relation.Binary.Structures.d_refl_34 (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_symmetric_40
           (coe MAlonzo.Code.Relation.Binary.Structures.d_sym_36 (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_transitive_50
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_38 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.isDecEquivalence
  d_isDecEquivalence_76 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
  d_isDecEquivalence_76 ~v0 ~v1 ~v2 ~v3 v4
    = du_isDecEquivalence_76 v4
  du_isDecEquivalence_76 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsDecEquivalence_44
  du_isDecEquivalence_76 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsDecEquivalence'46'constructor_3083
        (coe
           du_isEquivalence_56
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_50
              (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_decidable_112
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d__'8799'__52 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.isPreorder
  d_isPreorder_100 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  d_isPreorder_100 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 = du_isPreorder_100 v6
  du_isPreorder_100 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPreorder_70
  du_isPreorder_100 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPreorder'46'constructor_4003
        (coe
           du_isEquivalence_56
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isEquivalence_80
              (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_reflexive_28
           (MAlonzo.Code.Relation.Binary.Structures.d_reflexive_82 (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_transitive_50
           (coe MAlonzo.Code.Relation.Binary.Structures.d_trans_84 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.isPartialOrder
  d_isPartialOrder_142 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  d_isPartialOrder_142 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6
    = du_isPartialOrder_142 v6
  du_isPartialOrder_142 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174 ->
    MAlonzo.Code.Relation.Binary.Structures.T_IsPartialOrder_174
  du_isPartialOrder_142 v0
    = coe
        MAlonzo.Code.Relation.Binary.Structures.C_IsPartialOrder'46'constructor_9853
        (coe
           du_isPreorder_100
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_isPreorder_182 (coe v0)))
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_antisymmetric_64
           (coe
              MAlonzo.Code.Relation.Binary.Structures.d_antisym_184 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.setoid
  d_setoid_188 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_setoid_188 ~v0 ~v1 v2 = du_setoid_188 v2
  du_setoid_188 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_setoid_188 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Setoid'46'constructor_733
        (coe
           du_isEquivalence_56
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isEquivalence_60 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.decSetoid
  d_decSetoid_192 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
  d_decSetoid_192 ~v0 ~v1 v2 = du_decSetoid_192 v2
  du_decSetoid_192 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_DecSetoid_84
  du_decSetoid_192 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_DecSetoid'46'constructor_1389
        (coe
           du_isDecEquivalence_76
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isDecEquivalence_100
              (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.preorder
  d_preorder_196 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
  d_preorder_196 ~v0 ~v1 ~v2 v3 = du_preorder_196 v3
  du_preorder_196 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Preorder_132
  du_preorder_196 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Preorder'46'constructor_2267
        (coe
           du_isPreorder_100
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isPreorder_154 (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.poset
  d_poset_200 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
  d_poset_200 ~v0 ~v1 ~v2 v3 = du_poset_200 v3
  du_poset_200 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Poset_314
  du_poset_200 v0
    = coe
        MAlonzo.Code.Relation.Binary.Bundles.C_Poset'46'constructor_6389
        (coe
           du_isPartialOrder_142
           (coe
              MAlonzo.Code.Relation.Binary.Bundles.d_isPartialOrder_336
              (coe v0)))
  -- Data.List.Relation.Binary.Pointwise.All-resp-Pointwise
  d_All'45'resp'45'Pointwise_206 ::
    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] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  d_All'45'resp'45'Pointwise_206 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
                                 v10
    = du_All'45'resp'45'Pointwise_206 v6 v7 v8 v9 v10
  du_All'45'resp'45'Pointwise_206 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44 ->
    MAlonzo.Code.Data.List.Relation.Unary.All.T_All_44
  du_All'45'resp'45'Pointwise_206 v0 v1 v2 v3 v4
    = case coe v3 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe
               seq (coe v4)
               (coe MAlonzo.Code.Data.List.Relation.Unary.All.C_'91''93'_50)
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
          -> case coe v1 of
               (:) v11 v12
                 -> case coe v2 of
                      (:) v13 v14
                        -> case coe v4 of
                             MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60 v17 v18
                               -> coe
                                    MAlonzo.Code.Data.List.Relation.Unary.All.C__'8759'__60
                                    (coe v0 v11 v13 v9 v17)
                                    (coe
                                       du_All'45'resp'45'Pointwise_206 (coe v0) (coe v12) (coe v14)
                                       (coe v10) (coe v18))
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.Any-resp-Pointwise
  d_Any'45'resp'45'Pointwise_222 ::
    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] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
  d_Any'45'resp'45'Pointwise_222 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
                                 v10
    = du_Any'45'resp'45'Pointwise_222 v6 v7 v8 v9 v10
  du_Any'45'resp'45'Pointwise_222 ::
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
    MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
  du_Any'45'resp'45'Pointwise_222 v0 v1 v2 v3 v4
    = case coe v3 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
          -> case coe v1 of
               (:) v11 v12
                 -> case coe v2 of
                      (:) v13 v14
                        -> case coe v4 of
                             MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46 v17
                               -> coe
                                    MAlonzo.Code.Data.List.Relation.Unary.Any.C_here_46
                                    (coe v0 v11 v13 v9 v17)
                             MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54 v17
                               -> coe
                                    MAlonzo.Code.Data.List.Relation.Unary.Any.C_there_54
                                    (coe
                                       du_Any'45'resp'45'Pointwise_222 (coe v0) (coe v12) (coe v14)
                                       (coe v10) (coe v17))
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.AllPairs-resp-Pointwise
  d_AllPairs'45'resp'45'Pointwise_240 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  d_AllPairs'45'resp'45'Pointwise_240 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
                                      v8 v9 v10
    = du_AllPairs'45'resp'45'Pointwise_240 v6 v7 v8 v9 v10
  du_AllPairs'45'resp'45'Pointwise_240 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20 ->
    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.T_AllPairs_20
  du_AllPairs'45'resp'45'Pointwise_240 v0 v1 v2 v3 v4
    = case coe v3 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe
               seq (coe v4)
               (coe
                  MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C_'91''93'_22)
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
          -> case coe v1 of
               (:) v11 v12
                 -> case coe v2 of
                      (:) v13 v14
                        -> case coe v0 of
                             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v15 v16
                               -> case coe v4 of
                                    MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28 v19 v20
                                      -> coe
                                           MAlonzo.Code.Data.List.Relation.Unary.AllPairs.Core.C__'8759'__28
                                           (coe
                                              du_All'45'resp'45'Pointwise_206 (coe v15 v13) (coe v12)
                                              (coe v14) (coe v10)
                                              (coe
                                                 MAlonzo.Code.Data.List.Relation.Unary.All.du_map_164
                                                 (coe (\ v21 -> coe v16 v21 v11 v13 v9)) (coe v12)
                                                 (coe v19)))
                                           (coe
                                              du_AllPairs'45'resp'45'Pointwise_240 (coe v0) (coe v12)
                                              (coe v14) (coe v10) (coe v20))
                                    _ -> MAlonzo.RTE.mazUnreachableError
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.Pointwise-length
  d_Pointwise'45'length_256 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_Pointwise'45'length_256 = erased
  -- Data.List.Relation.Binary.Pointwise.tabulate⁺
  d_tabulate'8314'_270 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    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 -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_tabulate'8314'_270 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 ~v7 ~v8 v9
    = du_tabulate'8314'_270 v6 v9
  du_tabulate'8314'_270 ::
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_tabulate'8314'_270 v0 v1
    = case coe v0 of
        0 -> coe
               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        _ -> let v2 = subInt (coe v0) (coe (1 :: Integer)) in
             coe
               (coe
                  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                  (coe v1 (coe MAlonzo.Code.Data.Fin.Base.C_zero_12))
                  (coe
                     du_tabulate'8314'_270 (coe v2)
                     (coe
                        (\ v3 -> coe v1 (coe MAlonzo.Code.Data.Fin.Base.C_suc_16 v3)))))
  -- Data.List.Relation.Binary.Pointwise.tabulate⁻
  d_tabulate'8315'_286 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    Integer ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
  d_tabulate'8315'_286 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 v9 v10
    = du_tabulate'8315'_286 v9 v10
  du_tabulate'8315'_286 ::
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
  du_tabulate'8315'_286 v0 v1
    = case coe v0 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v6 v7
          -> case coe v1 of
               MAlonzo.Code.Data.Fin.Base.C_zero_12 -> coe v6
               MAlonzo.Code.Data.Fin.Base.C_suc_16 v9
                 -> coe du_tabulate'8315'_286 (coe v7) (coe v9)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.++⁺
  d_'43''43''8314'_302 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'43''43''8314'_302 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 ~v9 v10 v11
    = du_'43''43''8314'_302 v6 v7 v10 v11
  du_'43''43''8314'_302 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'43''43''8314'_302 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v3
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v8 v9
          -> case coe v0 of
               (:) v10 v11
                 -> case coe v1 of
                      (:) v12 v13
                        -> coe
                             MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                             v8
                             (coe du_'43''43''8314'_302 (coe v11) (coe v13) (coe v9) (coe v3))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.++-cancelˡ
  d_'43''43''45'cancel'737'_314 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'43''43''45'cancel'737'_314 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
    = du_'43''43''45'cancel'737'_314 v6 v7
  du_'43''43''45'cancel'737'_314 ::
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'43''43''45'cancel'737'_314 v0 v1
    = case coe v0 of
        [] -> coe v1
        (:) v2 v3
          -> case coe v1 of
               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v8 v9
                 -> coe du_'43''43''45'cancel'737'_314 (coe v3) (coe v9)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.++-cancelʳ
  d_'43''43''45'cancel'691'_328 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'43''43''45'cancel'691'_328 ~v0 ~v1 ~v2 ~v3 ~v4 v5 v6 v7
    = du_'43''43''45'cancel'691'_328 v5 v6 v7
  du_'43''43''45'cancel'691'_328 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'43''43''45'cancel'691'_328 v0 v1 v2
    = case coe v0 of
        []
          -> case coe v1 of
               []
                 -> coe
                      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
               (:) v3 v4
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                      erased
               _ -> MAlonzo.RTE.mazUnreachableError
        (:) v3 v4
          -> case coe v1 of
               []
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                      erased
               (:) v5 v6
                 -> case coe v2 of
                      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v11 v12
                        -> coe
                             MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                             v11
                             (coe du_'43''43''45'cancel'691'_328 (coe v4) (coe v6) (coe v12))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.concat⁺
  d_concat'8314'_362 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_concat'8314'_362 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8
    = du_concat'8314'_362 v6 v7 v8
  du_concat'8314'_362 ::
    [[AgdaAny]] ->
    [[AgdaAny]] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_concat'8314'_362 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v2
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v7 v8
          -> case coe v0 of
               (:) v9 v10
                 -> case coe v1 of
                      (:) v11 v12
                        -> coe
                             du_'43''43''8314'_302 (coe v9) (coe v11) (coe v7)
                             (coe du_concat'8314'_362 (coe v10) (coe v12) (coe v8))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.reverseAcc⁺
  d_reverseAcc'8314'_368 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_reverseAcc'8314'_368 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9 v10
                         v11
    = du_reverseAcc'8314'_368 v8 v9 v10 v11
  du_reverseAcc'8314'_368 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_reverseAcc'8314'_368 v0 v1 v2 v3
    = case coe v3 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v2
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v8 v9
          -> case coe v0 of
               (:) v10 v11
                 -> case coe v1 of
                      (:) v12 v13
                        -> coe
                             du_reverseAcc'8314'_368 (coe v11) (coe v13)
                             (coe
                                MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                v8 v2)
                             (coe v9)
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.ʳ++⁺
  d_'691''43''43''8314'_378 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'691''43''43''8314'_378 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 ~v8 ~v9 v10
                            v11
    = du_'691''43''43''8314'_378 v6 v7 v10 v11
  du_'691''43''43''8314'_378 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'691''43''43''8314'_378 v0 v1 v2 v3
    = coe du_reverseAcc'8314'_368 (coe v0) (coe v1) (coe v3) (coe v2)
  -- Data.List.Relation.Binary.Pointwise.reverse⁺
  d_reverse'8314'_384 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_reverse'8314'_384 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7
    = du_reverse'8314'_384 v6 v7
  du_reverse'8314'_384 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_reverse'8314'_384 v0 v1
    = coe
        du_reverseAcc'8314'_368 (coe v0) (coe v1)
        (coe
           MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
  -- Data.List.Relation.Binary.Pointwise.map⁺
  d_map'8314'_394 ::
    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 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    [AgdaAny] ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_map'8314'_394 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11
                  ~v12 ~v13 v14
    = du_map'8314'_394 v10 v11 v14
  du_map'8314'_394 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_map'8314'_394 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v2
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v7 v8
          -> case coe v0 of
               (:) v9 v10
                 -> case coe v1 of
                      (:) v11 v12
                        -> coe
                             MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                             v7 (coe du_map'8314'_394 (coe v10) (coe v12) (coe v8))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.map⁻
  d_map'8315'_416 ::
    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 ->
    () ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    [AgdaAny] ->
    [AgdaAny] ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_map'8315'_416 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11
                  ~v12 ~v13 v14
    = du_map'8315'_416 v10 v11 v14
  du_map'8315'_416 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_map'8315'_416 v0 v1 v2
    = case coe v0 of
        []
          -> coe
               seq (coe v1)
               (coe
                  seq (coe v2)
                  (coe
                     MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56))
        (:) v3 v4
          -> case coe v1 of
               (:) v5 v6
                 -> case coe v2 of
                      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v11 v12
                        -> coe
                             MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                             v11 (coe du_map'8315'_416 (coe v4) (coe v6) (coe v12))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.foldr⁺
  d_foldr'8314'_446 ::
    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 ->
     AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    AgdaAny
  d_foldr'8314'_446 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9 v10 v11 v12
                    v13 v14
    = du_foldr'8314'_446 v6 v7 v8 v9 v10 v11 v12 v13 v14
  du_foldr'8314'_446 ::
    [AgdaAny] ->
    [AgdaAny] ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    AgdaAny ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    AgdaAny
  du_foldr'8314'_446 v0 v1 v2 v3 v4 v5 v6 v7 v8
    = case coe v8 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v7
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v13 v14
          -> case coe v0 of
               (:) v15 v16
                 -> case coe v1 of
                      (:) v17 v18
                        -> coe
                             v4 v15 v17
                             (coe
                                MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v2) (coe v5)
                                (coe v16))
                             (coe
                                MAlonzo.Code.Data.List.Base.du_foldr_216 (coe v3) (coe v6)
                                (coe v18))
                             v13
                             (coe
                                du_foldr'8314'_446 (coe v16) (coe v18) (coe v2) (coe v3) (coe v4)
                                (coe v5) (coe v6) (coe v7) (coe v14))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise._.filter⁺
  d_filter'8314'_492 ::
    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 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    (AgdaAny -> ()) ->
    (AgdaAny -> ()) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    (AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_filter'8314'_492 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 ~v8 ~v9 v10 v11
                     ~v12 ~v13 v14 v15 v16
    = du_filter'8314'_492 v10 v11 v14 v15 v16
  du_filter'8314'_492 ::
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    (AgdaAny ->
     MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_filter'8314'_492 v0 v1 v2 v3 v4
    = case coe v4 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
          -> coe v4
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v9 v10
          -> case coe v2 of
               (:) v11 v12
                 -> case coe v3 of
                      (:) v13 v14
                        -> let v15 = coe v0 v11 in
                           coe
                             (let v16 = coe v1 v13 in
                              coe
                                (case coe v15 of
                                   MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v17 v18
                                     -> if coe v17
                                          then case coe v16 of
                                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v19 v20
                                                   -> if coe v19
                                                        then coe
                                                               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                                                               v9
                                                               (coe
                                                                  du_filter'8314'_492 (coe v0)
                                                                  (coe v1) (coe v12) (coe v14)
                                                                  (coe v10))
                                                        else coe
                                                               seq (coe v18)
                                                               (coe
                                                                  seq (coe v20)
                                                                  (coe
                                                                     MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                                                     erased))
                                                 _ -> MAlonzo.RTE.mazUnreachableError
                                          else (case coe v16 of
                                                  MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v19 v20
                                                    -> if coe v19
                                                         then coe
                                                                seq (coe v18)
                                                                (coe
                                                                   seq (coe v20)
                                                                   (coe
                                                                      MAlonzo.Code.Relation.Nullary.Negation.Core.du_contradiction_44
                                                                      erased))
                                                         else coe
                                                                du_filter'8314'_492 (coe v0) (coe v1)
                                                                (coe v12) (coe v14) (coe v10)
                                                  _ -> MAlonzo.RTE.mazUnreachableError)
                                   _ -> MAlonzo.RTE.mazUnreachableError))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.replicate⁺
  d_replicate'8314'_548 ::
    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 ->
    Integer ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_replicate'8314'_548 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 ~v6 ~v7 v8 v9
    = du_replicate'8314'_548 v8 v9
  du_replicate'8314'_548 ::
    AgdaAny ->
    Integer ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_replicate'8314'_548 v0 v1
    = case coe v1 of
        0 -> coe
               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56
        _ -> let v2 = subInt (coe v1) (coe (1 :: Integer)) in
             coe
               (coe
                  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                  v0 (coe du_replicate'8314'_548 (coe v0) (coe v2)))
  -- Data.List.Relation.Binary.Pointwise.lookup⁻
  d_lookup'8315'_560 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    (AgdaAny -> AgdaAny -> ()) ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
     MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_lookup'8315'_560 ~v0 ~v1 v2 ~v3 ~v4 v5 ~v6 ~v7 ~v8 v9
    = du_lookup'8315'_560 v2 v5 v9
  du_lookup'8315'_560 ::
    [AgdaAny] ->
    [AgdaAny] ->
    (MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
     MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_lookup'8315'_560 v0 v1 v2
    = case coe v0 of
        []
          -> coe
               seq (coe v1)
               (coe
                  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C_'91''93'_56)
        (:) v3 v4
          -> case coe v1 of
               (:) v5 v6
                 -> coe
                      MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62
                      (coe
                         v2 (coe MAlonzo.Code.Data.Fin.Base.C_zero_12)
                         (coe MAlonzo.Code.Data.Fin.Base.C_zero_12) erased)
                      (coe
                         du_lookup'8315'_560 (coe v4) (coe v6)
                         (coe
                            (\ v7 v8 v9 ->
                               coe
                                 v2 (coe MAlonzo.Code.Data.Fin.Base.C_suc_16 v7)
                                 (coe MAlonzo.Code.Data.Fin.Base.C_suc_16 v8) erased)))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.lookup⁺
  d_lookup'8314'_572 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
  d_lookup'8314'_572 ~v0 ~v1 ~v2 ~v3 ~v4 ~v5 v6 v7 v8 v9
    = du_lookup'8314'_572 v6 v7 v8 v9
  du_lookup'8314'_572 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 -> AgdaAny
  du_lookup'8314'_572 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.C__'8759'__62 v8 v9
          -> case coe v0 of
               (:) v10 v11
                 -> case coe v1 of
                      (:) v12 v13
                        -> case coe v3 of
                             MAlonzo.Code.Data.Fin.Base.C_zero_12 -> coe v8
                             MAlonzo.Code.Data.Fin.Base.C_suc_16 v15
                               -> coe du_lookup'8314'_572 (coe v11) (coe v13) (coe v9) (coe v15)
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Data.List.Relation.Binary.Pointwise.Pointwise-≡⇒≡
  d_Pointwise'45''8801''8658''8801'_580 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_Pointwise'45''8801''8658''8801'_580 = erased
  -- Data.List.Relation.Binary.Pointwise.≡⇒Pointwise-≡
  d_'8801''8658'Pointwise'45''8801'_590 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'8801''8658'Pointwise'45''8801'_590 ~v0 ~v1 v2 ~v3 ~v4
    = du_'8801''8658'Pointwise'45''8801'_590 v2
  du_'8801''8658'Pointwise'45''8801'_590 ::
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'8801''8658'Pointwise'45''8801'_590 v0
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Properties.du_refl_30
        erased (coe v0)
  -- Data.List.Relation.Binary.Pointwise.Pointwise-≡↔≡
  d_Pointwise'45''8801''8596''8801'_592 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
  d_Pointwise'45''8801''8596''8801'_592 ~v0 ~v1
    = du_Pointwise'45''8801''8596''8801'_592
  du_Pointwise'45''8801''8596''8801'_592 ::
    MAlonzo.Code.Function.Bundles.T_Inverse_1960
  du_Pointwise'45''8801''8596''8801'_592
    = coe
        MAlonzo.Code.Function.Bundles.C_Inverse'46'constructor_38621
        (coe (\ v0 -> v0)) (coe (\ v0 -> v0)) erased
        (\ v0 v1 v2 -> coe du_'8801''8658'Pointwise'45''8801'_590 v0)
        (coe
           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 erased
           (coe
              (\ v0 v1 v2 ->
                 coe du_'8801''8658'Pointwise'45''8801'_590 (coe v1))))
  