{-# 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.Relation.Unary.Properties 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.Sigma
import qualified MAlonzo.Code.Agda.Builtin.Unit
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Empty
import qualified MAlonzo.Code.Data.Product
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Relation.Nullary
import qualified MAlonzo.Code.Relation.Nullary.Negation.Core
import qualified MAlonzo.Code.Relation.Nullary.Product
import qualified MAlonzo.Code.Relation.Nullary.Sum

-- Relation.Unary.Properties.∅?
d_'8709''63'_20 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8709''63'_20 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Dec_32
d_'8709''63'_20 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Dec_32
du_'8709''63'_20
du_'8709''63'_20 :: MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8709''63'_20 :: T_Dec_32
du_'8709''63'_20
  = (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)
-- Relation.Unary.Properties.∅-Empty
d_'8709''45'Empty_22 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Data.Empty.T_'8869'_4 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8709''45'Empty_22 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_'8869'_4 -> T_'8869'_4
d_'8709''45'Empty_22 = T_Level_18 -> T_Level_18 -> AgdaAny -> T_'8869'_4 -> T_'8869'_4
forall a. a
erased
-- Relation.Unary.Properties.∁∅-Universal
d_'8705''8709''45'Universal_26 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  MAlonzo.Code.Data.Empty.T_'8869'_4 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8705''8709''45'Universal_26 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_'8869'_4 -> T_'8869'_4
d_'8705''8709''45'Universal_26 = T_Level_18 -> T_Level_18 -> AgdaAny -> T_'8869'_4 -> T_'8869'_4
forall a. a
erased
-- Relation.Unary.Properties.U?
d_U'63'_32 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_U'63'_32 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Dec_32
d_U'63'_32 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Dec_32
du_U'63'_32
du_U'63'_32 :: MAlonzo.Code.Relation.Nullary.T_Dec_32
du_U'63'_32 :: T_Dec_32
du_U'63'_32
  = (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_true_10)
      ((AgdaAny -> T_Reflects_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         AgdaAny -> T_Reflects_14
MAlonzo.Code.Relation.Nullary.C_of'696'_22
         (T_Level_18 -> AgdaAny
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8))
-- Relation.Unary.Properties.U-Universal
d_U'45'Universal_34 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_U'45'Universal_34 :: T_Level_18 -> T_Level_18 -> AgdaAny -> T_Level_18
d_U'45'Universal_34 ~T_Level_18
v0 ~T_Level_18
v1 ~AgdaAny
v2 = T_Level_18
du_U'45'Universal_34
du_U'45'Universal_34 :: MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_U'45'Universal_34 :: T_Level_18
du_U'45'Universal_34 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Relation.Unary.Properties.∁U-Empty
d_'8705'U'45'Empty_38 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  AgdaAny ->
  (MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6 ->
   MAlonzo.Code.Data.Empty.T_'8869'_4) ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8705'U'45'Empty_38 :: T_Level_18
-> T_Level_18
-> AgdaAny
-> (T_Level_18 -> T_'8869'_4)
-> T_'8869'_4
d_'8705'U'45'Empty_38 = T_Level_18
-> T_Level_18
-> AgdaAny
-> (T_Level_18 -> T_'8869'_4)
-> T_'8869'_4
forall a. a
erased
-- Relation.Unary.Properties.∅-⊆
d_'8709''45''8838'_46 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> MAlonzo.Code.Data.Empty.T_'8869'_4 -> AgdaAny
d_'8709''45''8838'_46 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> T_'8869'_4
-> AgdaAny
d_'8709''45''8838'_46 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~T_'8869'_4
v5
  = AgdaAny
du_'8709''45''8838'_46
du_'8709''45''8838'_46 :: AgdaAny
du_'8709''45''8838'_46 :: AgdaAny
du_'8709''45''8838'_46 = AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties.⊆-U
d_'8838''45'U_52 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
d_'8838''45'U_52 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> T_Level_18
d_'8838''45'U_52 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 ~AgdaAny
v5 = T_Level_18
du_'8838''45'U_52
du_'8838''45'U_52 :: MAlonzo.Code.Agda.Builtin.Unit.T_'8868'_6
du_'8838''45'U_52 :: T_Level_18
du_'8838''45'U_52 = T_Level_18 -> T_Level_18
forall a b. a -> b
coe T_Level_18
MAlonzo.Code.Agda.Builtin.Unit.C_tt_8
-- Relation.Unary.Properties.⊆-refl
d_'8838''45'refl_56 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''45'refl_56 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''45'refl_56 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny
v4 AgdaAny
v5
  = AgdaAny -> AgdaAny
du_'8838''45'refl_56 AgdaAny
v5
du_'8838''45'refl_56 :: AgdaAny -> AgdaAny
du_'8838''45'refl_56 :: AgdaAny -> AgdaAny
du_'8838''45'refl_56 AgdaAny
v0 = AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v0
-- Relation.Unary.Properties.⊆-trans
d_'8838''45'trans_60 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
d_'8838''45'trans_60 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_'8838''45'trans_60 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
  = (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_60 AgdaAny -> AgdaAny -> AgdaAny
v6 AgdaAny -> AgdaAny -> AgdaAny
v7 AgdaAny
v8 AgdaAny
v9
du_'8838''45'trans_60 ::
  (AgdaAny -> AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_60 :: (AgdaAny -> AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
du_'8838''45'trans_60 AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 AgdaAny
v3 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v1 AgdaAny
v2 ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
v0 AgdaAny
v2 AgdaAny
v3)
-- Relation.Unary.Properties.⊂-asym
d_'8834''45'asym_68 ::
  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.Sigma.T_Σ_14 ->
  MAlonzo.Code.Data.Empty.T_'8869'_4
d_'8834''45'asym_68 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_'8869'_4
d_'8834''45'asym_68 = T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> T_Σ_14
-> T_Σ_14
-> T_'8869'_4
forall a. a
erased
-- Relation.Unary.Properties.∁?
d_'8705''63'_74 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d_'8705''63'_74 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> AgdaAny
-> T_Dec_32
d_'8705''63'_74 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~AgdaAny -> T_Level_18
v3 AgdaAny -> T_Dec_32
v4 AgdaAny
v5 = (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du_'8705''63'_74 AgdaAny -> T_Dec_32
v4 AgdaAny
v5
du_'8705''63'_74 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du_'8705''63'_74 :: (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du_'8705''63'_74 AgdaAny -> T_Dec_32
v0 AgdaAny
v1
  = (T_Dec_32 -> T_Dec_32) -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Negation.Core.du_'172''63'_64
      ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v1)
-- Relation.Unary.Properties._∪?_
d__'8746''63'__84 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8746''63'__84 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> AgdaAny
-> T_Dec_32
d__'8746''63'__84 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> T_Dec_32
v6 AgdaAny -> T_Dec_32
v7 AgdaAny
v8
  = (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du__'8746''63'__84 AgdaAny -> T_Dec_32
v6 AgdaAny -> T_Dec_32
v7 AgdaAny
v8
du__'8746''63'__84 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8746''63'__84 :: (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du__'8746''63'__84 AgdaAny -> T_Dec_32
v0 AgdaAny -> T_Dec_32
v1 AgdaAny
v2
  = (T_Dec_32 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Sum.du__'8846''45'dec__32 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v2)
      ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v1 AgdaAny
v2)
-- Relation.Unary.Properties._∩?_
d__'8745''63'__96 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8745''63'__96 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> AgdaAny
-> T_Dec_32
d__'8745''63'__96 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~AgdaAny -> T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 AgdaAny -> T_Dec_32
v6 AgdaAny -> T_Dec_32
v7 AgdaAny
v8
  = (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du__'8745''63'__96 AgdaAny -> T_Dec_32
v6 AgdaAny -> T_Dec_32
v7 AgdaAny
v8
du__'8745''63'__96 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8745''63'__96 :: (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
du__'8745''63'__96 AgdaAny -> T_Dec_32
v0 AgdaAny -> T_Dec_32
v1 AgdaAny
v2
  = (T_Dec_32 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
      T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
      ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v2) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v1 AgdaAny
v2)
-- Relation.Unary.Properties._×?_
d__'215''63'__108 ::
  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 -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'215''63'__108 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Σ_14
-> T_Dec_32
d__'215''63'__108 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> T_Dec_32
v8 AgdaAny -> T_Dec_32
v9 T_Σ_14
v10
  = (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'215''63'__108 AgdaAny -> T_Dec_32
v8 AgdaAny -> T_Dec_32
v9 T_Σ_14
v10
du__'215''63'__108 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'215''63'__108 :: (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'215''63'__108 AgdaAny -> T_Dec_32
v0 AgdaAny -> T_Dec_32
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
        -> (T_Dec_32 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Product.du__'215''45'dec__30
             ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v3) ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v1 AgdaAny
v4)
      T_Σ_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._⊙?_
d__'8857''63'__122 ::
  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 -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8857''63'__122 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T_Σ_14
-> T_Dec_32
d__'8857''63'__122 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 ~AgdaAny -> T_Level_18
v7 AgdaAny -> T_Dec_32
v8 AgdaAny -> T_Dec_32
v9 T_Σ_14
v10
  = (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'8857''63'__122 AgdaAny -> T_Dec_32
v8 AgdaAny -> T_Dec_32
v9 T_Σ_14
v10
du__'8857''63'__122 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8857''63'__122 :: (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'8857''63'__122 AgdaAny -> T_Dec_32
v0 AgdaAny -> T_Dec_32
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
        -> (T_Dec_32 -> T_Dec_32 -> T_Dec_32)
-> AgdaAny -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe
             T_Dec_32 -> T_Dec_32 -> T_Dec_32
MAlonzo.Code.Relation.Nullary.Sum.du__'8846''45'dec__32 ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v3)
             ((AgdaAny -> T_Dec_32) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v1 AgdaAny
v4)
      T_Σ_14
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._⊎?_
d__'8846''63'__136 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> ()) ->
  (AgdaAny -> ()) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'8846''63'__136 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Level_18)
-> (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32)
-> T__'8846'__30
-> T_Dec_32
d__'8846''63'__136 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~AgdaAny -> T_Level_18
v5 ~AgdaAny -> T_Level_18
v6 AgdaAny -> T_Dec_32
v7 AgdaAny -> T_Dec_32
v8 T__'8846'__30
v9
  = (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T__'8846'__30 -> T_Dec_32
du__'8846''63'__136 AgdaAny -> T_Dec_32
v7 AgdaAny -> T_Dec_32
v8 T__'8846'__30
v9
du__'8846''63'__136 ::
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  (AgdaAny -> MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'8846''63'__136 :: (AgdaAny -> T_Dec_32)
-> (AgdaAny -> T_Dec_32) -> T__'8846'__30 -> T_Dec_32
du__'8846''63'__136 AgdaAny -> T_Dec_32
v0 AgdaAny -> T_Dec_32
v1 T__'8846'__30
v2
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v2 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v3 -> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v0 AgdaAny
v3
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v3 -> (AgdaAny -> T_Dec_32) -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe AgdaAny -> T_Dec_32
v1 AgdaAny
v3
      T__'8846'__30
_ -> T_Dec_32
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Relation.Unary.Properties._~?
d__'126''63'_152 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 -> ()) ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
d__'126''63'_152 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (T_Σ_14 -> T_Level_18)
-> (T_Σ_14 -> T_Dec_32)
-> T_Σ_14
-> T_Dec_32
d__'126''63'_152 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Level_18
v4 ~T_Σ_14 -> T_Level_18
v5 T_Σ_14 -> T_Dec_32
v6 T_Σ_14
v7
  = (T_Σ_14 -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'126''63'_152 T_Σ_14 -> T_Dec_32
v6 T_Σ_14
v7
du__'126''63'_152 ::
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Relation.Nullary.T_Dec_32) ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
  MAlonzo.Code.Relation.Nullary.T_Dec_32
du__'126''63'_152 :: (T_Σ_14 -> T_Dec_32) -> T_Σ_14 -> T_Dec_32
du__'126''63'_152 T_Σ_14 -> T_Dec_32
v0 T_Σ_14
v1
  = (T_Σ_14 -> T_Dec_32) -> AgdaAny -> T_Dec_32
forall a b. a -> b
coe T_Σ_14 -> T_Dec_32
v0 ((T_Σ_14 -> T_Σ_14) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.du_swap_386 (T_Σ_14 -> AgdaAny
forall a b. a -> b
coe T_Σ_14
v1))