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.Equality.Propositional 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.Relation.Binary.Equality.Setoid qualified
  import MAlonzo.Code.Data.List.Relation.Binary.Pointwise qualified
  import MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base 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.Relation.Binary.Bundles qualified
  import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties qualified
  import MAlonzo.Code.Relation.Binary.Structures qualified
  import MAlonzo.Code.Relation.Nullary.Decidable.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.Equality.Propositional._._≋_
  d__'8779'__18 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> [AgdaAny] -> [AgdaAny] -> ()
  d__'8779'__18 = erased
  -- Data.List.Relation.Binary.Equality.Propositional._.++-cancelʳ
  d_'43''43''45'cancel'691'_20 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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'_20 ~v0 ~v1
    = du_'43''43''45'cancel'691'_20
  du_'43''43''45'cancel'691'_20 ::
    [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
  du_'43''43''45'cancel'691'_20 v0
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'43''43''45'cancel'691'_164
  -- Data.List.Relation.Binary.Equality.Propositional._.++-cancelˡ
  d_'43''43''45'cancel'737'_22 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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'_22 ~v0 ~v1
    = du_'43''43''45'cancel'737'_22
  du_'43''43''45'cancel'737'_22 ::
    [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
  du_'43''43''45'cancel'737'_22 v0 v1 v2
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'43''43''45'cancel'737'_154
        v0
  -- Data.List.Relation.Binary.Equality.Propositional._.++⁺
  d_'43''43''8314'_24 ::
    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 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'43''43''8314'_24 ~v0 ~v1 = du_'43''43''8314'_24
  du_'43''43''8314'_24 ::
    [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
  du_'43''43''8314'_24 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'43''43''8314'_146
        v0 v1
  -- Data.List.Relation.Binary.Equality.Propositional._.Unique-resp-≋
  d_Unique'45'resp'45''8779'_26 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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_Unique'45'resp'45''8779'_26 ~v0 ~v1
    = du_Unique'45'resp'45''8779'_26
  du_Unique'45'resp'45''8779'_26 ::
    [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_Unique'45'resp'45''8779'_26
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_Unique'45'resp'45''8779'_72
  -- Data.List.Relation.Binary.Equality.Propositional._.concat⁺
  d_concat'8314'_28 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [[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'_28 ~v0 ~v1 = du_concat'8314'_28
  du_concat'8314'_28 ::
    [[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'_28
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_concat'8314'_170
  -- Data.List.Relation.Binary.Equality.Propositional._.filter⁺
  d_filter'8314'_30 ::
    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 ->
     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'_30 ~v0 ~v1 = du_filter'8314'_30
  du_filter'8314'_30 ::
    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 ->
     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
  du_filter'8314'_30 v0 v1 v2 v3 v4 v5 v6
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_filter'8314'_206
        v2 v4 v5 v6
  -- Data.List.Relation.Binary.Equality.Propositional._.foldr⁺
  d_foldr'8314'_32 ::
    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 ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
    [AgdaAny] ->
    [AgdaAny] ->
    AgdaAny ->
    AgdaAny ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_foldr'8314'_32 = erased
  -- Data.List.Relation.Binary.Equality.Propositional._.map⁺
  d_map'8314'_34 ::
    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_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> 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'_34 ~v0 ~v1 = du_map'8314'_34
  du_map'8314'_34 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44 ->
    (AgdaAny -> AgdaAny) ->
    (AgdaAny ->
     AgdaAny ->
     MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> 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
  du_map'8314'_34 v0 v1 v2 v3 v4 v5 v6 v7
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_map'8314'_102
        v4 v5 v6 v7
  -- Data.List.Relation.Binary.Equality.Propositional._.reverse⁺
  d_reverse'8314'_36 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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'_36 ~v0 ~v1 = du_reverse'8314'_36
  du_reverse'8314'_36 ::
    [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'_36
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_reverse'8314'_224
  -- Data.List.Relation.Binary.Equality.Propositional._.tabulate⁺
  d_tabulate'8314'_38 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_tabulate'8314'_38 ~v0 ~v1 = du_tabulate'8314'_38
  du_tabulate'8314'_38 ::
    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.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_tabulate'8314'_38 v0 v1 v2
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_tabulate'8314'_184
        v0
  -- Data.List.Relation.Binary.Equality.Propositional._.Pointwise.Pointwise
  d_Pointwise_39 a0 a1 a2 a3 a4 a5 a6 a7 a8 a9 = ()
  -- Data.List.Relation.Binary.Equality.Propositional._.tabulate⁻
  d_tabulate'8315'_40 ::
    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.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
  d_tabulate'8315'_40 = erased
  -- Data.List.Relation.Binary.Equality.Propositional._.ʳ++⁺
  d_'691''43''43''8314'_42 ::
    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 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'691''43''43''8314'_42 ~v0 ~v1 = du_'691''43''43''8314'_42
  du_'691''43''43''8314'_42 ::
    [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
  du_'691''43''43''8314'_42 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'691''43''43''8314'_218
        v0 v1
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-isEquivalence
  d_'8779''45'isEquivalence_44 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  d_'8779''45'isEquivalence_44 ~v0 ~v1
    = du_'8779''45'isEquivalence_44
  du_'8779''45'isEquivalence_44 ::
    MAlonzo.Code.Relation.Binary.Structures.T_IsEquivalence_26
  du_'8779''45'isEquivalence_44
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'isEquivalence_68
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-length
  d_'8779''45'length_46 ::
    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_'8779''45'length_46 = erased
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-refl
  d_'8779''45'refl_48 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  d_'8779''45'refl_48 ~v0 ~v1 = du_'8779''45'refl_48
  du_'8779''45'refl_48 ::
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'8779''45'refl_48
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'refl_60
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-reflexive
  d_'8779''45'reflexive_50 ::
    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_'8779''45'reflexive_50 ~v0 ~v1 = du_'8779''45'reflexive_50
  du_'8779''45'reflexive_50 ::
    [AgdaAny] ->
    [AgdaAny] ->
    MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'8779''45'reflexive_50 v0 v1 v2
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'reflexive_62
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
        v0
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-setoid
  d_'8779''45'setoid_52 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () -> MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  d_'8779''45'setoid_52 ~v0 ~v1 = du_'8779''45'setoid_52
  du_'8779''45'setoid_52 ::
    MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_44
  du_'8779''45'setoid_52
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'setoid_70
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-sym
  d_'8779''45'sym_54 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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_'8779''45'sym_54 ~v0 ~v1 = du_'8779''45'sym_54
  du_'8779''45'sym_54 ::
    [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_'8779''45'sym_54
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'sym_64
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Data.List.Relation.Binary.Equality.Propositional._.≋-trans
  d_'8779''45'trans_56 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    [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_'8779''45'trans_56 ~v0 ~v1 = du_'8779''45'trans_56
  du_'8779''45'trans_56 ::
    [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
  du_'8779''45'trans_56
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'trans_66
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
  -- Data.List.Relation.Binary.Equality.Propositional._.Pointwise.All-resp-Pointwise
  d_All'45'resp'45'Pointwise_64 ::
    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) ->
    [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_64 ~v0 ~v1
    = du_All'45'resp'45'Pointwise_64
  du_All'45'resp'45'Pointwise_64 ::
    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
  du_All'45'resp'45'Pointwise_64 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_All'45'resp'45'Pointwise_206
        v6 v7 v8 v9 v10
  -- Data.List.Relation.Binary.Equality.Propositional._.Pointwise.AllPairs-resp-Pointwise
  d_AllPairs'45'resp'45'Pointwise_66 ::
    MAlonzo.Code.Agda.Primitive.T_Level_18 ->
    () ->
    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_66 ~v0 ~v1
    = du_AllPairs'45'resp'45'Pointwise_66
  du_AllPairs'45'resp'45'Pointwise_66 ::
    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
  du_AllPairs'45'resp'45'Pointwise_66 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9
                                      v10
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_AllPairs'45'resp'45'Pointwise_240
        v6 v7 v8 v9 v10
  -- Data.List.Relation.Binary.Equality.Propositional._.Pointwise.Any-resp-Pointwise
  d_Any'45'resp'45'Pointwise_68 ::
    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) ->
    [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_68 ~v0 ~v1
    = du_Any'45'resp'45'Pointwise_68
  du_Any'45'resp'45'Pointwise_68 ::
    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
  du_Any'45'resp'45'Pointwise_68 v0 v1 v2 v3 v4 v5 v6 v7 v8 v9 v10
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Pointwise.du_Any'45'resp'45'Pointwise_222
        v6 v7 v8 v9 v10
  -- Data.List.Relation.Binary.Equality.Propositional.≋⇒≡
  d_'8779''8658''8801'_72 ::
    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_'8779''8658''8801'_72 = erased
  -- Data.List.Relation.Binary.Equality.Propositional.≡⇒≋
  d_'8801''8658''8779'_78 ::
    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''8779'_78 ~v0 ~v1 v2 ~v3 ~v4
    = du_'8801''8658''8779'_78 v2
  du_'8801''8658''8779'_78 ::
    [AgdaAny] ->
    MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
  du_'8801''8658''8779'_78 v0
    = coe
        MAlonzo.Code.Data.List.Relation.Binary.Equality.Setoid.du_'8779''45'refl_60
        (coe
           MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
        (coe v0)
  