{-# 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.Nullary.Decidable 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.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Primitive
import qualified MAlonzo.Code.Data.Irrelevant
import qualified MAlonzo.Code.Function.Bundles
import qualified MAlonzo.Code.Relation.Binary.Bundles
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core

-- Relation.Nullary.Decidable.map
d_map_18 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_map_18 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Dec_20
-> T_Dec_20
d_map_18 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 T_Equivalence_1858
v4 = T_Equivalence_1858 -> T_Dec_20 -> T_Dec_20
du_map_18 T_Equivalence_1858
v4
du_map_18 ::
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_map_18 :: T_Equivalence_1858 -> T_Dec_20 -> T_Dec_20
du_map_18 T_Equivalence_1858
v0
  = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
      ((T_Equivalence_1858 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1858 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_1868 (T_Equivalence_1858 -> Any
forall a b. a -> b
coe T_Equivalence_1858
v0))
      ((T_Equivalence_1858 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Equivalence_1858 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_from_1870 (T_Equivalence_1858 -> Any
forall a b. a -> b
coe T_Equivalence_1858
v0))
-- Relation.Nullary.Decidable._._.Eq₁._≈_
d__'8776'__130 ::
  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.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__130 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> Any
-> Any
-> T_Level_18
d__'8776'__130 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable._._.Eq₂._≈_
d__'8776'__156 ::
  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.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  AgdaAny -> AgdaAny -> ()
d__'8776'__156 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> Any
-> Any
-> T_Level_18
d__'8776'__156 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> Any
-> Any
-> T_Level_18
forall a. a
erased
-- Relation.Nullary.Decidable._.via-injection
d_via'45'injection_180 ::
  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.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Relation.Binary.Bundles.T_Setoid_46 ->
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_via'45'injection_180 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Setoid_46
-> T_Setoid_46
-> T_Injection_842
-> (Any -> Any -> T_Dec_20)
-> Any
-> Any
-> T_Dec_20
d_via'45'injection_180 ~T_Level_18
v0 ~T_Level_18
v1 ~T_Level_18
v2 ~T_Level_18
v3 ~T_Setoid_46
v4 ~T_Setoid_46
v5 T_Injection_842
v6 Any -> Any -> T_Dec_20
v7 Any
v8 Any
v9
  = T_Injection_842
-> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20
du_via'45'injection_180 T_Injection_842
v6 Any -> Any -> T_Dec_20
v7 Any
v8 Any
v9
du_via'45'injection_180 ::
  MAlonzo.Code.Function.Bundles.T_Injection_842 ->
  (AgdaAny ->
   AgdaAny ->
   MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20) ->
  AgdaAny ->
  AgdaAny -> MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_via'45'injection_180 :: T_Injection_842
-> (Any -> Any -> T_Dec_20) -> Any -> Any -> T_Dec_20
du_via'45'injection_180 T_Injection_842
v0 Any -> Any -> T_Dec_20
v1 Any
v2 Any
v3
  = ((Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20)
-> Any -> Any -> Any -> T_Dec_20
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_178
      ((T_Injection_842 -> Any -> Any -> Any -> Any)
-> T_Injection_842 -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_842 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_injective_854 T_Injection_842
v0 Any
v2 Any
v3)
      ((T_Injection_842 -> Any -> Any -> Any -> Any)
-> T_Injection_842 -> Any -> Any -> Any
forall a b. a -> b
coe T_Injection_842 -> Any -> Any -> Any -> Any
MAlonzo.Code.Function.Bundles.d_cong_852 T_Injection_842
v0 Any
v2 Any
v3)
      ((Any -> Any -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
         Any -> Any -> T_Dec_20
v1 ((T_Injection_842 -> Any -> Any) -> T_Injection_842 -> Any -> Any
forall a b. a -> b
coe T_Injection_842 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_850 T_Injection_842
v0 Any
v2)
         ((T_Injection_842 -> Any -> Any) -> T_Injection_842 -> Any -> Any
forall a b. a -> b
coe T_Injection_842 -> Any -> Any
MAlonzo.Code.Function.Bundles.d_to_850 T_Injection_842
v0 Any
v3))
-- Relation.Nullary.Decidable.True-↔
d_True'45''8596'_190 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
d_True'45''8596'_190 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> T_Inverse_2122
d_True'45''8596'_190 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any -> Any -> T__'8801'__12
v3 = T_Dec_20 -> T_Inverse_2122
du_True'45''8596'_190 T_Dec_20
v2
du_True'45''8596'_190 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Function.Bundles.T_Inverse_2122
du_True'45''8596'_190 :: T_Dec_20 -> T_Inverse_2122
du_True'45''8596'_190 T_Dec_20
v0
  = ((Any -> Any) -> (Any -> Any) -> T_Inverse_2122)
-> Any -> Any -> T_Inverse_2122
forall a b. a -> b
coe
      (Any -> Any) -> (Any -> Any) -> T_Inverse_2122
MAlonzo.Code.Function.Bundles.du_mk'8596''8347''8242'_2542
      ((T_Dec_20 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Dec_20 -> Any -> Any
du_to_200 (T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
v0)) ((T_Dec_20 -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe T_Dec_20 -> Any -> Any
du_from_202 (T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
v0))
-- Relation.Nullary.Decidable._.to
d_to_200 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> AgdaAny
d_to_200 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> Any
d_to_200 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any -> Any -> T__'8801'__12
v3 = T_Dec_20 -> Any -> Any
du_to_200 T_Dec_20
v2
du_to_200 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny
du_to_200 :: T_Dec_20 -> Any -> Any
du_to_200 T_Dec_20
v0 Any
v1
  = (T_Dec_20 -> Any) -> Any -> Any
forall a b. a -> b
coe
      T_Dec_20 -> Any
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_toWitness_144
      (T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
v0)
-- Relation.Nullary.Decidable._.from
d_from_202 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> AgdaAny
d_from_202 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> Any
d_from_202 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any -> Any -> T__'8801'__12
v3 = T_Dec_20 -> Any -> Any
du_from_202 T_Dec_20
v2
du_from_202 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> AgdaAny
du_from_202 :: T_Dec_20 -> Any -> Any
du_from_202 T_Dec_20
v0
  = (T_Dec_20 -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
      T_Dec_20 -> Any -> Any
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_fromWitness_150
      (T_Dec_20 -> Any
forall a b. a -> b
coe T_Dec_20
v0)
-- Relation.Nullary.Decidable._.to-from
d_to'45'from_206 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_to'45'from_206 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
d_to'45'from_206 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable._.from-to
d_from'45'to_214 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_from'45'to_214 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> T_Dec_20
-> Any
-> T__'8801'__12
d_from'45'to_214 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> T_Dec_20
-> Any
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.isYes≗does
d_isYes'8791'does_218 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_isYes'8791'does_218 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> T__'8801'__12
d_isYes'8791'does_218 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-true
d_dec'45'true_222 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'true_222 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
d_dec'45'true_222 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-false
d_dec'45'false_232 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'false_232 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
d_dec'45'false_232 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-yes-recompute
d_dec'45'yes'45'recompute_244 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'yes'45'recompute_244 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
d_dec'45'yes'45'recompute_244 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-yes-irr
d_dec'45'yes'45'irr_258 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny ->
   AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'yes'45'irr_258 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
d_dec'45'yes'45'irr_258 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> Any -> T__'8801'__12)
-> Any
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.dec-yes
d_dec'45'yes_270 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  AgdaAny -> MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_dec'45'yes_270 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> Any -> T_Σ_14
d_dec'45'yes_270 ~T_Level_18
v0 ~T_Level_18
v1 T_Dec_20
v2 ~Any
v3 = T_Dec_20 -> T_Σ_14
du_dec'45'yes_270 T_Dec_20
v2
du_dec'45'yes_270 ::
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_dec'45'yes_270 :: T_Dec_20 -> T_Σ_14
du_dec'45'yes_270 T_Dec_20
v0
  = (Any -> Any -> T_Σ_14) -> Any -> Any -> T_Σ_14
forall a b. a -> b
coe
      Any -> Any -> T_Σ_14
MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
      ((T_Dec_20 -> Any -> Any) -> T_Dec_20 -> Any -> Any
forall a b. a -> b
coe
         T_Dec_20 -> Any -> Any
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_recompute_54 T_Dec_20
v0
         Any
forall a. a
erased)
      Any
forall a. a
erased
-- Relation.Nullary.Decidable.dec-no
d_dec'45'no_280 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  (AgdaAny -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dec'45'no_280 :: T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
d_dec'45'no_280 = T_Level_18
-> T_Level_18
-> T_Dec_20
-> (Any -> T_Irrelevant_20)
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.⌊⌋-map′
d_'8970''8971''45'map'8242'_296 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  (AgdaAny -> AgdaAny) ->
  (AgdaAny -> AgdaAny) ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_'8970''8971''45'map'8242'_296 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Dec_20
-> T__'8801'__12
d_'8970''8971''45'map'8242'_296 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> (Any -> Any)
-> (Any -> Any)
-> T_Dec_20
-> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.does-≡
d_does'45''8801'_308 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_does'45''8801'_308 :: T_Level_18 -> T_Level_18 -> T_Dec_20 -> T_Dec_20 -> T__'8801'__12
d_does'45''8801'_308 = T_Level_18 -> T_Level_18 -> T_Dec_20 -> T_Dec_20 -> T__'8801'__12
forall a. a
erased
-- Relation.Nullary.Decidable.does-⇔
d_does'45''8660'_322 ::
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Agda.Primitive.T_Level_18 ->
  () ->
  MAlonzo.Code.Function.Bundles.T_Equivalence_1858 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_does'45''8660'_322 :: T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Dec_20
-> T_Dec_20
-> T__'8801'__12
d_does'45''8660'_322 = T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Level_18
-> T_Equivalence_1858
-> T_Dec_20
-> T_Dec_20
-> T__'8801'__12
forall a. a
erased