{-# 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.Maybe.Relation.Unary.Any where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Bool
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Function.Equivalence
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Decidable

-- Data.Maybe.Relation.Unary.Any.Any
d_Any_18 :: p -> p -> p -> p -> p -> ()
d_Any_18 p
a0 p
a1 p
a2 p
a3 p
a4 = ()
newtype T_Any_18 = C_just_30 AgdaAny
-- Data.Maybe.Relation.Unary.Any._.drop-just
d_drop'45'just_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> (AgdaAny -> ()) -> AgdaAny -> T_Any_18 -> AgdaAny
d_drop'45'just_46 :: () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> T_Any_18 -> AgdaAny
d_drop'45'just_46 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4 T_Any_18
v5 = T_Any_18 -> AgdaAny
du_drop'45'just_46 T_Any_18
v5
du_drop'45'just_46 :: T_Any_18 -> AgdaAny
du_drop'45'just_46 :: T_Any_18 -> AgdaAny
du_drop'45'just_46 T_Any_18
v0
  = case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v0 of
      C_just_30 AgdaAny
v2 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2
      T_Any_18
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.just-equivalence
d_just'45'equivalence_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Function.Equivalence.T_Equivalence_16
d_just'45'equivalence_52 :: () -> () -> () -> (AgdaAny -> ()) -> AgdaAny -> T_Equivalence_16
d_just'45'equivalence_52 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~AgdaAny
v4
  = T_Equivalence_16
du_just'45'equivalence_52
du_just'45'equivalence_52 ::
  MAlonzo.Code.Function.Equivalence.T_Equivalence_16
du_just'45'equivalence_52 :: T_Equivalence_16
du_just'45'equivalence_52
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16)
-> AgdaAny -> AgdaAny -> T_Equivalence_16
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> T_Equivalence_16
MAlonzo.Code.Function.Equivalence.du_equivalence_56 ((AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)
      ((T_Any_18 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Any_18 -> AgdaAny
du_drop'45'just_46)
-- Data.Maybe.Relation.Unary.Any._.map
d_map_58 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> T_Any_18 -> T_Any_18
d_map_58 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
d_map_58 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 ~()
v4 ~AgdaAny -> ()
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 T_Any_18
v8 = (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 AgdaAny -> AgdaAny -> AgdaAny
v6 Maybe AgdaAny
v7 T_Any_18
v8
du_map_58 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> Maybe AgdaAny -> T_Any_18 -> T_Any_18
du_map_58 AgdaAny -> AgdaAny -> AgdaAny
v0 Maybe AgdaAny
v1 T_Any_18
v2
  = case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v2 of
      C_just_30 AgdaAny
v4
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
               -> (AgdaAny -> T_Any_18) -> AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v5 AgdaAny
v4)
             Maybe AgdaAny
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.satisfied
d_satisfied_66 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_satisfied_66 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_satisfied_66 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 Maybe AgdaAny
v4 T_Any_18
v5 = Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_satisfied_66 Maybe AgdaAny
v4 T_Any_18
v5
du_satisfied_66 ::
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfied_66 :: Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_satisfied_66 Maybe AgdaAny
v0 T_Any_18
v1
  = case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v1 of
      C_just_30 AgdaAny
v3
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v4
               -> (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.du_'45''44'__112 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3)
             Maybe AgdaAny
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Any_18
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.zipWith
d_zipWith_90 ::
  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 -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
d_zipWith_90 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny
-> T_Σ_14
-> T_Any_18
d_zipWith_90 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> ()
v5 ~AgdaAny -> ()
v6 ~AgdaAny -> ()
v7 AgdaAny -> T_Σ_14 -> AgdaAny
v8 Maybe AgdaAny
v9 T_Σ_14
v10
  = (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 AgdaAny -> T_Σ_14 -> AgdaAny
v8 Maybe AgdaAny
v9 T_Σ_14
v10
du_zipWith_90 ::
  (AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> AgdaAny) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
du_zipWith_90 :: (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 AgdaAny -> T_Σ_14 -> AgdaAny
v0 Maybe AgdaAny
v1 T_Σ_14
v2
  = case T_Σ_14 -> T_Σ_14
forall a b. a -> b
coe T_Σ_14
v2 of
      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v3 AgdaAny
v4
        -> case AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny
v3 of
             C_just_30 AgdaAny
v6
               -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
                    MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v7
                      -> case AgdaAny -> T_Any_18
forall a b. a -> b
coe AgdaAny
v4 of
                           C_just_30 AgdaAny
v9
                             -> (AgdaAny -> T_Any_18) -> AgdaAny -> T_Any_18
forall a b. a -> b
coe
                                  AgdaAny -> T_Any_18
C_just_30
                                  ((AgdaAny -> T_Σ_14 -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     AgdaAny -> T_Σ_14 -> AgdaAny
v0 AgdaAny
v7
                                     ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        AgdaAny -> AgdaAny -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                                        (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
                           T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
                    Maybe AgdaAny
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Any_18
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Σ_14
_ -> T_Any_18
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.unzipWith
d_unzipWith_98 ::
  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.Agda.Builtin.Sigma.T_Σ_14) ->
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_unzipWith_98 :: ()
-> ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_unzipWith_98 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~()
v4 ~AgdaAny -> ()
v5 ~AgdaAny -> ()
v6 ~AgdaAny -> ()
v7 AgdaAny -> AgdaAny -> T_Σ_14
v8 Maybe AgdaAny
v9 T_Any_18
v10
  = (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 AgdaAny -> AgdaAny -> T_Σ_14
v8 Maybe AgdaAny
v9 T_Any_18
v10
du_unzipWith_98 ::
  (AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14) ->
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_unzipWith_98 :: (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 AgdaAny -> AgdaAny -> T_Σ_14
v0 Maybe AgdaAny
v1 T_Any_18
v2
  = case T_Any_18 -> T_Any_18
forall a b. a -> b
coe T_Any_18
v2 of
      C_just_30 AgdaAny
v4
        -> case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
             MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148 ((AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)
                    ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v6 -> (AgdaAny -> T_Any_18) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30)) ((AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> T_Σ_14
v0 AgdaAny
v5 AgdaAny
v4)
             Maybe AgdaAny
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Any_18
_ -> T_Σ_14
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.zip
d_zip_120 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
d_zip_120 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Σ_14
-> T_Any_18
d_zip_120 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> ()
v5 Maybe AgdaAny
v6 = Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zip_120 Maybe AgdaAny
v6
du_zip_120 ::
  Maybe AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> T_Any_18
du_zip_120 :: Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zip_120 Maybe AgdaAny
v0 = ((AgdaAny -> T_Σ_14 -> AgdaAny)
 -> Maybe AgdaAny -> T_Σ_14 -> T_Any_18)
-> AgdaAny -> AgdaAny -> T_Σ_14 -> T_Any_18
forall a b. a -> b
coe (AgdaAny -> T_Σ_14 -> AgdaAny)
-> Maybe AgdaAny -> T_Σ_14 -> T_Any_18
du_zipWith_90 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0)
-- Data.Maybe.Relation.Unary.Any._.unzip
d_unzip_122 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_unzip_122 :: ()
-> ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> ())
-> Maybe AgdaAny
-> T_Any_18
-> T_Σ_14
d_unzip_122 ~()
v0 ~()
v1 ~()
v2 ~()
v3 ~AgdaAny -> ()
v4 ~AgdaAny -> ()
v5 Maybe AgdaAny
v6 = Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzip_122 Maybe AgdaAny
v6
du_unzip_122 ::
  Maybe AgdaAny -> T_Any_18 -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_unzip_122 :: Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzip_122 Maybe AgdaAny
v0
  = ((AgdaAny -> AgdaAny -> T_Σ_14)
 -> Maybe AgdaAny -> T_Any_18 -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T_Any_18 -> T_Σ_14
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> T_Σ_14)
-> Maybe AgdaAny -> T_Any_18 -> T_Σ_14
du_unzipWith_98 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v1 AgdaAny
v2 -> AgdaAny
v2)) (Maybe AgdaAny -> AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v0)
-- Data.Maybe.Relation.Unary.Any._.dec
d_dec_136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_dec_136 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> T_Dec_32)
-> Maybe AgdaAny
-> T_Dec_32
d_dec_136 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5 = (AgdaAny -> T_Dec_32) -> Maybe AgdaAny -> T_Dec_32
du_dec_136 AgdaAny -> T_Dec_32
v4 Maybe AgdaAny
v5
du_dec_136 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  Maybe AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_dec_136 :: (AgdaAny -> T_Dec_32) -> Maybe AgdaAny -> T_Dec_32
du_dec_136 AgdaAny -> T_Dec_32
v0 Maybe AgdaAny
v1
  = case Maybe AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe Maybe AgdaAny
v1 of
      MAlonzo.Code.Agda.Builtin.Maybe.C_just_16 AgdaAny
v2
        -> (T_Equivalence_16 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             T_Equivalence_16 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Decidable.du_map_14
             (T_Equivalence_16 -> AgdaAny
forall a b. a -> b
coe T_Equivalence_16
du_just'45'equivalence_52) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v2)
      Maybe AgdaAny
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18
        -> (Bool -> T_Reflects_14 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             Bool -> T_Reflects_14 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.C__because__46
             (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
             (T_Reflects_14 -> AgdaAny
forall a b. a -> b
coe T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'8319'_26)
      Maybe AgdaAny
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Data.Maybe.Relation.Unary.Any._.irrelevant
d_irrelevant_144 ::
  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) ->
  Maybe AgdaAny ->
  T_Any_18 ->
  T_Any_18 -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_irrelevant_144 :: ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
-> T__'8801'__12
d_irrelevant_144 = ()
-> ()
-> ()
-> (AgdaAny -> ())
-> (AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'__12)
-> Maybe AgdaAny
-> T_Any_18
-> T_Any_18
-> T__'8801'__12
forall a. a
erased
-- Data.Maybe.Relation.Unary.Any._.satisfiable
d_satisfiable_152 ::
  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.Builtin.Sigma.T_Σ_14
d_satisfiable_152 :: () -> () -> () -> (AgdaAny -> ()) -> T_Σ_14 -> T_Σ_14
d_satisfiable_152 ~()
v0 ~()
v1 ~()
v2 ~AgdaAny -> ()
v3 T_Σ_14
v4 = T_Σ_14 -> T_Σ_14
du_satisfiable_152 T_Σ_14
v4
du_satisfiable_152 ::
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_satisfiable_152 :: T_Σ_14 -> T_Σ_14
du_satisfiable_152 T_Σ_14
v0
  = ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_map_148
      ((AgdaAny -> Maybe AgdaAny) -> AgdaAny
forall a b. a -> b
coe AgdaAny -> Maybe AgdaAny
forall {a}. a -> Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_just_16)
      (\ AgdaAny
v1 AgdaAny
v2 -> (AgdaAny -> T_Any_18) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Any_18
C_just_30 AgdaAny
v2) (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v0)