{-# 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.Membership.Propositional.Properties.Core 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.List.Membership.Propositional qualified
import MAlonzo.Code.Data.List.Membership.Setoid qualified
import MAlonzo.Code.Data.List.Relation.Unary.Any qualified
import MAlonzo.Code.Function.Bundles qualified
import MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties 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.Membership.Propositional.Properties.Core.find-∈
d_find'45''8712'_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_find'45''8712'_26 :: T_Level_18
-> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Any_34 -> T__'8801'__12
d_find'45''8712'_26 = T_Level_18
-> T_Level_18 -> AgdaAny -> [AgdaAny] -> T_Any_34 -> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core._.map∘find
d_map'8728'find_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  (AgdaAny ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_map'8728'find_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> (AgdaAny -> T__'8801'__12 -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
d_map'8728'find_56 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> (AgdaAny -> T__'8801'__12 -> AgdaAny)
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core._.find∘map
d_find'8728'map_80 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_find'8728'map_80 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
d_find'8728'map_80 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core._.∃∈-Any
d_'8707''8712''45'Any_106 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
d_'8707''8712''45'Any_106 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Σ_14
-> T_Any_34
d_'8707''8712''45'Any_106 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 [AgdaAny]
v4 T_Σ_14
v5
  = [AgdaAny] -> T_Σ_14 -> T_Any_34
du_'8707''8712''45'Any_106 [AgdaAny]
v4 T_Σ_14
v5
du_'8707''8712''45'Any_106 ::
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34
du_'8707''8712''45'Any_106 :: [AgdaAny] -> T_Σ_14 -> T_Any_34
du_'8707''8712''45'Any_106 [AgdaAny]
v0 T_Σ_14
v1
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v1 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v2 AgdaAny
v3
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> (AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34)
-> AgdaAny -> [AgdaAny] -> AgdaAny -> AgdaAny -> T_Any_34
forall a b. a -> b
coe
                    AgdaAny -> [AgdaAny] -> T_Any_34 -> AgdaAny -> T_Any_34
MAlonzo.Code.Data.List.Membership.Propositional.du_lose_50 AgdaAny
v2 [AgdaAny]
v0 AgdaAny
v4
                    AgdaAny
v5
             T_Σ_14
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Any_34
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.List.Membership.Propositional.Properties.Core._.∃∈-Any∘find
d_'8707''8712''45'Any'8728'find_116 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8707''8712''45'Any'8728'find_116 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T__'8801'__12
d_'8707''8712''45'Any'8728'find_116 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core._.find∘∃∈-Any
d_find'8728''8707''8712''45'Any_124 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_find'8728''8707''8712''45'Any_124 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Σ_14
-> T__'8801'__12
d_find'8728''8707''8712''45'Any_124 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Σ_14
-> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core._.Any↔
d_Any'8596'_144 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
d_Any'8596'_144 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Inverse_1960
d_Any'8596'_144 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 [AgdaAny]
v4 = [AgdaAny] -> T_Inverse_1960
du_Any'8596'_144 [AgdaAny]
v4
du_Any'8596'_144 ::
  [AgdaAny] -> MAlonzo.Code.Function.Bundles.T_Inverse_1960
du_Any'8596'_144 :: [AgdaAny] -> T_Inverse_1960
du_Any'8596'_144 [AgdaAny]
v0
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960)
-> AgdaAny -> AgdaAny -> T_Inverse_1960
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Inverse_1960
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2366
      (([AgdaAny] -> T_Σ_14 -> T_Any_34) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> T_Σ_14 -> T_Any_34
du_'8707''8712''45'Any_106 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0))
      ((T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Setoid_44 -> [AgdaAny] -> T_Any_34 -> T_Σ_14
MAlonzo.Code.Data.List.Membership.Setoid.du_find_84
         (T_Setoid_44 -> AgdaAny
forall a b. a -> b
coe
            T_Setoid_44
MAlonzo.Code.Relation.Binary.PropositionalEquality.Properties.du_setoid_402)
         ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v0))
-- Data.List.Membership.Propositional.Properties.Core.lose∘find
d_lose'8728'find_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lose'8728'find_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T__'8801'__12
d_lose'8728'find_152 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> [AgdaAny]
-> T_Any_34
-> T__'8801'__12
forall a. a
erased
-- Data.List.Membership.Propositional.Properties.Core.find∘lose
d_find'8728'lose_164 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny ->
  [AgdaAny] ->
  MAlonzo.Code.Data.List.Relation.Unary.Any.T_Any_34 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_find'8728'lose_164 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
d_find'8728'lose_164 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> [AgdaAny]
-> T_Any_34
-> AgdaAny
-> T__'8801'__12
forall a. a
erased