{-# 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.Reflection.AST.Term 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.List
import qualified MAlonzo.Code.Agda.Builtin.Maybe
import qualified MAlonzo.Code.Agda.Builtin.Reflection
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Agda.Builtin.String
import qualified MAlonzo.Code.Data.List.Base
import qualified MAlonzo.Code.Data.List.Properties
import qualified MAlonzo.Code.Data.Nat.Properties
import qualified MAlonzo.Code.Data.Product.Base
import qualified MAlonzo.Code.Data.Product.Properties
import qualified MAlonzo.Code.Data.String.Properties
import qualified MAlonzo.Code.Reflection.AST.Abstraction
import qualified MAlonzo.Code.Reflection.AST.Argument
import qualified MAlonzo.Code.Reflection.AST.Argument.Visibility
import qualified MAlonzo.Code.Reflection.AST.Literal
import qualified MAlonzo.Code.Reflection.AST.Meta
import qualified MAlonzo.Code.Reflection.AST.Name
import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
import qualified MAlonzo.Code.Relation.Nullary.Reflects

-- Reflection.AST.Term.Clauses
d_Clauses_6 :: ()
d_Clauses_6 :: ()
d_Clauses_6 = ()
forall a. a
erased
-- Reflection.AST.Term.Telescope
d_Telescope_8 :: ()
d_Telescope_8 :: ()
d_Telescope_8 = ()
forall a. a
erased
-- Reflection.AST.Term.getName
d_getName_60 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 -> Maybe AgdaAny
d_getName_60 :: T_Term_154 -> Maybe AgdaAny
d_getName_60 T_Term_154
v0
  = let v1 :: b
v1 = Maybe AgdaAny -> b
forall a b. a -> b
coe Maybe AgdaAny
forall {a}. Maybe a
MAlonzo.Code.Agda.Builtin.Maybe.C_nothing_18 in
    AgdaAny -> Maybe AgdaAny
forall a b. a -> b
coe
      (case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v0 of
         MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v2 [T_Arg_88]
v3
           -> (AgdaAny -> Maybe AgdaAny) -> 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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
         MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v2 [T_Arg_88]
v3
           -> (AgdaAny -> Maybe AgdaAny) -> 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 -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2)
         T_Term_154
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)
-- Reflection.AST.Term._⋯⟨∷⟩_
d__'8943''10216''8759''10217'__70 ::
  Integer ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
d__'8943''10216''8759''10217'__70 :: Integer -> [T_Arg_88] -> [T_Arg_88]
d__'8943''10216''8759''10217'__70 Integer
v0 [T_Arg_88]
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> [T_Arg_88] -> [T_Arg_88]
forall a b. a -> b
coe [T_Arg_88]
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> [T_Arg_88]
forall a b. a -> b
coe
             ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                   ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                      (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)
                      ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                         (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                         (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                   (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216))
                ((Integer -> [T_Arg_88] -> [T_Arg_88])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> [T_Arg_88] -> [T_Arg_88]
d__'8943''10216''8759''10217'__70 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v1)))
-- Reflection.AST.Term._⋯⟅∷⟆_
d__'8943''10181''8759''10182'__78 ::
  Integer ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88]
d__'8943''10181''8759''10182'__78 :: Integer -> [T_Arg_88] -> [T_Arg_88]
d__'8943''10181''8759''10182'__78 Integer
v0 [T_Arg_88]
v1
  = case Integer -> Integer
forall a b. a -> b
coe Integer
v0 of
      Integer
0 -> [T_Arg_88] -> [T_Arg_88]
forall a b. a -> b
coe [T_Arg_88]
v1
      Integer
_ -> let v2 :: Integer
v2 = Integer -> Integer -> Integer
subInt (Integer -> Integer
forall a b. a -> b
coe Integer
v0) (Integer -> Integer
forall a b. a -> b
coe (Integer
1 :: Integer)) in
           AgdaAny -> [T_Arg_88]
forall a b. a -> b
coe
             ((AgdaAny -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                ((T_ArgInfo_76 -> AgdaAny -> T_Arg_88)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_ArgInfo_76 -> AgdaAny -> T_Arg_88
MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98
                   ((T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Visibility_48 -> T_Modality_68 -> T_ArgInfo_76
MAlonzo.Code.Agda.Builtin.Reflection.C_arg'45'info_82
                      (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52)
                      ((T_Relevance_56 -> T_Quantity_62 -> T_Modality_68)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Relevance_56 -> T_Quantity_62 -> T_Modality_68
MAlonzo.Code.Agda.Builtin.Reflection.C_modality_74
                         (T_Relevance_56 -> AgdaAny
forall a b. a -> b
coe T_Relevance_56
MAlonzo.Code.Agda.Builtin.Reflection.C_relevant_58)
                         (T_Quantity_62 -> AgdaAny
forall a b. a -> b
coe T_Quantity_62
MAlonzo.Code.Agda.Builtin.Reflection.C_quantity'45'ω_66)))
                   (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216))
                ((Integer -> [T_Arg_88] -> [T_Arg_88])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe Integer -> [T_Arg_88] -> [T_Arg_88]
d__'8943''10181''8759''10182'__78 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v1)))
-- Reflection.AST.Term.stripPis
d_stripPis_86 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_stripPis_86 :: T_Term_154 -> T_Σ_14
d_stripPis_86 T_Term_154
v0
  = let v1 :: t
v1
          = (AgdaAny -> AgdaAny -> T_Σ_14) -> AgdaAny -> AgdaAny -> t
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]
forall {a}. [a]
MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16) (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v0) in
    AgdaAny -> T_Σ_14
forall a b. a -> b
coe
      (case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v0 of
         MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v2 T_Abs_112
v3
           -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v3 of
                MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v4 AgdaAny
v5
                  -> ((AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14)
-> AgdaAny -> T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
                       (AgdaAny -> AgdaAny) -> T_Σ_14 -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_map'8321'_138
                       ((AgdaAny -> [AgdaAny] -> [AgdaAny]) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> [AgdaAny] -> [AgdaAny]
forall {a}. a -> [a] -> [a]
MAlonzo.Code.Agda.Builtin.List.C__'8759'__22
                          ((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 (T_String_6 -> AgdaAny
forall a b. a -> b
coe T_String_6
v4) (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v2)))
                       (T_Term_154 -> T_Σ_14
d_stripPis_86 (AgdaAny -> T_Term_154
forall a b. a -> b
coe AgdaAny
v5))
                T_Abs_112
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
         T_Term_154
_ -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v1)
-- Reflection.AST.Term.prependLams
d_prependLams_98 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154
d_prependLams_98 :: [T_Σ_14] -> T_Term_154 -> T_Term_154
d_prependLams_98 [T_Σ_14]
v0 T_Term_154
v1
  = ((AgdaAny -> AgdaAny -> AgdaAny)
 -> AgdaAny -> [AgdaAny] -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Term_154
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> [AgdaAny] -> AgdaAny
MAlonzo.Code.Data.List.Base.du_foldr_216
      ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
         (\ AgdaAny
v2 AgdaAny
v3 ->
            case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
              MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
                -> (T_Visibility_48 -> T_Abs_112 -> T_Term_154)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                     T_Visibility_48 -> T_Abs_112 -> T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)
                     ((T_String_6 -> AgdaAny -> T_Abs_112)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                        T_String_6 -> AgdaAny -> T_Abs_112
MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
              T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError))
      (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v1) (([AgdaAny] -> [AgdaAny]) -> [T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_reverse_460 [T_Σ_14]
v0)
-- Reflection.AST.Term.prependHLams
d_prependHLams_112 ::
  [MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154
d_prependHLams_112 :: [T_String_6] -> T_Term_154 -> T_Term_154
d_prependHLams_112 [T_String_6]
v0
  = ([T_Σ_14] -> T_Term_154 -> T_Term_154)
-> AgdaAny -> T_Term_154 -> T_Term_154
forall a b. a -> b
coe
      [T_Σ_14] -> T_Term_154 -> T_Term_154
d_prependLams_98
      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (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
v1)
                 (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_hidden_52)))
         ([T_String_6] -> AgdaAny
forall a b. a -> b
coe [T_String_6]
v0))
-- Reflection.AST.Term.prependVLams
d_prependVLams_118 ::
  [MAlonzo.Code.Agda.Builtin.String.T_String_6] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154
d_prependVLams_118 :: [T_String_6] -> T_Term_154 -> T_Term_154
d_prependVLams_118 [T_String_6]
v0
  = ([T_Σ_14] -> T_Term_154 -> T_Term_154)
-> AgdaAny -> T_Term_154 -> T_Term_154
forall a b. a -> b
coe
      [T_Σ_14] -> T_Term_154 -> T_Term_154
d_prependLams_98
      (((AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny])
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> [AgdaAny] -> [AgdaAny]
MAlonzo.Code.Data.List.Base.du_map_22
         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v1 ->
               (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
v1)
                 (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
MAlonzo.Code.Agda.Builtin.Reflection.C_visible_50)))
         ([T_String_6] -> AgdaAny
forall a b. a -> b
coe [T_String_6]
v0))
-- Reflection.AST.Term.clause-injective₁
d_clause'45'injective'8321'_136 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_clause'45'injective'8321'_136 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
d_clause'45'injective'8321'_136 = [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.clause-injective₂
d_clause'45'injective'8322'_150 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_clause'45'injective'8322'_150 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
d_clause'45'injective'8322'_150 = [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.clause-injective₃
d_clause'45'injective'8323'_164 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_clause'45'injective'8323'_164 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
d_clause'45'injective'8323'_164 = [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.clause-injective
d_clause'45'injective_178 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_clause'45'injective_178 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T_Term_154
-> T_Term_154
-> T__'8801'__12
-> T_Σ_14
d_clause'45'injective_178 ~[T_Σ_14]
v0 ~[T_Σ_14]
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3 ~T_Term_154
v4 ~T_Term_154
v5
  = T__'8801'__12 -> T_Σ_14
du_clause'45'injective_178
du_clause'45'injective_178 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_clause'45'injective_178 :: T__'8801'__12 -> T_Σ_14
du_clause'45'injective_178
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased
      (((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased)
-- Reflection.AST.Term.absurd-clause-injective₁
d_absurd'45'clause'45'injective'8321'_188 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_absurd'45'clause'45'injective'8321'_188 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_absurd'45'clause'45'injective'8321'_188 = [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.absurd-clause-injective₂
d_absurd'45'clause'45'injective'8322'_198 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_absurd'45'clause'45'injective'8322'_198 :: [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_absurd'45'clause'45'injective'8322'_198 = [T_Σ_14]
-> [T_Σ_14]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.absurd-clause-injective
d_absurd'45'clause'45'injective_208 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_absurd'45'clause'45'injective_208 :: [T_Σ_14]
-> [T_Σ_14] -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_absurd'45'clause'45'injective_208 ~[T_Σ_14]
v0 ~[T_Σ_14]
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3
  = T__'8801'__12 -> T_Σ_14
du_absurd'45'clause'45'injective_208
du_absurd'45'clause'45'injective_208 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_absurd'45'clause'45'injective_208 :: T__'8801'__12 -> T_Σ_14
du_absurd'45'clause'45'injective_208
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term._≟-AbsTerm_
d__'8799''45'AbsTerm__210 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'AbsTerm__210 :: T_Abs_112 -> T_Abs_112 -> T_Dec_20
d__'8799''45'AbsTerm__210 T_Abs_112
v0 T_Abs_112
v1
  = case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v2 AgdaAny
v3
        -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v4 AgdaAny
v5
               -> (T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Abstraction.du_unAbs'45'dec_46 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v0)
                    (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v1) ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             T_Abs_112
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Abs_112
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-AbsType_
d__'8799''45'AbsType__212 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'AbsType__212 :: T_Abs_112 -> T_Abs_112 -> T_Dec_20
d__'8799''45'AbsType__212 T_Abs_112
v0 T_Abs_112
v1
  = case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v2 AgdaAny
v3
        -> case T_Abs_112 -> T_Abs_112
forall a b. a -> b
coe T_Abs_112
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_abs_122 T_String_6
v4 AgdaAny
v5
               -> (T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Abs_112 -> T_Abs_112 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Abstraction.du_unAbs'45'dec_46 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v0)
                    (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v1) ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             T_Abs_112
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Abs_112
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-ArgTerm_
d__'8799''45'ArgTerm__214 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'ArgTerm__214 :: T_Arg_88 -> T_Arg_88 -> T_Dec_20
d__'8799''45'ArgTerm__214 T_Arg_88
v0 T_Arg_88
v1
  = case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v2 AgdaAny
v3
        -> case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v4 AgdaAny
v5
               -> (T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.du_unArg'45'dec_84 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v0)
                    (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v1) ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-ArgType_
d__'8799''45'ArgType__216 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'ArgType__216 :: T_Arg_88 -> T_Arg_88 -> T_Dec_20
d__'8799''45'ArgType__216 T_Arg_88
v0 T_Arg_88
v1
  = case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v2 AgdaAny
v3
        -> case T_Arg_88 -> T_Arg_88
forall a b. a -> b
coe T_Arg_88
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v4 AgdaAny
v5
               -> (T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.du_unArg'45'dec_84 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v0)
                    (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v1) ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
             T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Args_
d__'8799''45'Args__218 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Args__218 :: [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 [T_Arg_88]
v0 [T_Arg_88]
v1
  = case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v0 of
      []
        -> case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             (:) AgdaAny
v2 [AgdaAny]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             (:) AgdaAny
v4 [AgdaAny]
v5
               -> (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Data.List.Properties.du_'8759''45'dec_52
                    ((T_Arg_88 -> T_Arg_88 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> T_Arg_88 -> T_Dec_20
d__'8799''45'ArgTerm__214 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5))
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Clause_
d__'8799''45'Clause__220 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Clause__220 :: T_Clause_160 -> T_Clause_160 -> T_Dec_20
d__'8799''45'Clause__220 T_Clause_160
v0 T_Clause_160
v1
  = case T_Clause_160 -> T_Clause_160
forall a b. a -> b
coe T_Clause_160
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 [T_Σ_14]
v2 [T_Arg_88]
v3 T_Term_154
v4
        -> case T_Clause_160 -> T_Clause_160
forall a b. a -> b
coe T_Clause_160
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 [T_Σ_14]
v5 [T_Arg_88]
v6 T_Term_154
v7
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_clause'45'injective_178)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       (([T_Σ_14] -> [T_Σ_14] -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [T_Σ_14] -> T_Dec_20
d__'8799''45'Telescope__280 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v2) ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v5))
                       ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                          (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Patterns__228 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v6))
                          ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v4) (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v7))))
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd'45'clause_278 [T_Σ_14]
v5 [T_Arg_88]
v6
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Clause_160
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_absurd'45'clause_278 [T_Σ_14]
v2 [T_Arg_88]
v3
        -> case T_Clause_160 -> T_Clause_160
forall a b. a -> b
coe T_Clause_160
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_clause_272 [T_Σ_14]
v4 [T_Arg_88]
v5 T_Term_154
v6
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd'45'clause_278 [T_Σ_14]
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_absurd'45'clause'45'injective_208)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       (([T_Σ_14] -> [T_Σ_14] -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [T_Σ_14] -> T_Dec_20
d__'8799''45'Telescope__280 ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v2) ([T_Σ_14] -> AgdaAny
forall a b. a -> b
coe [T_Σ_14]
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Patterns__228 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             T_Clause_160
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Clause_160
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Clauses_
d__'8799''45'Clauses__222 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Clauses__222 :: [T_Clause_160] -> [T_Clause_160] -> T_Dec_20
d__'8799''45'Clauses__222 [T_Clause_160]
v0 [T_Clause_160]
v1
  = case [T_Clause_160] -> [AgdaAny]
forall a b. a -> b
coe [T_Clause_160]
v0 of
      []
        -> case [T_Clause_160] -> [AgdaAny]
forall a b. a -> b
coe [T_Clause_160]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             (:) AgdaAny
v2 [AgdaAny]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> case [T_Clause_160] -> [AgdaAny]
forall a b. a -> b
coe [T_Clause_160]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             (:) AgdaAny
v4 [AgdaAny]
v5
               -> (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Data.List.Properties.du_'8759''45'dec_52
                    ((T_Clause_160 -> T_Clause_160 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Clause_160 -> T_Clause_160 -> T_Dec_20
d__'8799''45'Clause__220 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                    (([T_Clause_160] -> [T_Clause_160] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Clause_160] -> [T_Clause_160] -> T_Dec_20
d__'8799''45'Clauses__222 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v5))
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟_
d__'8799'__224 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799'__224 :: T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 T_Term_154
v0 T_Term_154
v1
  = case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v2 [T_Arg_88]
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_var'45'injective_350)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v2 [T_Arg_88]
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_con'45'injective_380)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Reflection.AST.Name.d__'8799'__12 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v2 [T_Arg_88]
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_def'45'injective_410)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Reflection.AST.Name.d__'8799'__12 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v2 T_Abs_112
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_lam'45'injective_470)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((T_Visibility_48 -> T_Visibility_48 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Visibility_48 -> T_Visibility_48 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.Visibility.d__'8799'__8
                          (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
v2) (T_Visibility_48 -> AgdaAny
forall a b. a -> b
coe T_Visibility_48
v4))
                       ((T_Abs_112 -> T_Abs_112 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Abs_112 -> T_Abs_112 -> T_Dec_20
d__'8799''45'AbsTerm__210 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v3) (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v2 [T_Arg_88]
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_pat'45'lam'45'injective_500)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       (([T_Clause_160] -> [T_Clause_160] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Clause_160] -> [T_Clause_160] -> T_Dec_20
d__'8799''45'Clauses__222 ([T_Clause_160] -> AgdaAny
forall a b. a -> b
coe [T_Clause_160]
v2) ([T_Clause_160] -> AgdaAny
forall a b. a -> b
coe [T_Clause_160]
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v2 T_Abs_112
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_pi'45'injective_530)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((T_Arg_88 -> T_Arg_88 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> T_Arg_88 -> T_Dec_20
d__'8799''45'ArgType__216 (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v2) (T_Arg_88 -> AgdaAny
forall a b. a -> b
coe T_Arg_88
v4))
                       ((T_Abs_112 -> T_Abs_112 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Abs_112 -> T_Abs_112 -> T_Dec_20
d__'8799''45'AbsType__212 (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v3) (T_Abs_112 -> AgdaAny
forall a b. a -> b
coe T_Abs_112
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v2
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v3 T_Abs_112
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v3 T_Abs_112
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Sort_156 -> T_Sort_156 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Sort_156 -> T_Sort_156 -> T_Dec_20
d__'8799''45'Sort__226 (T_Sort_156 -> AgdaAny
forall a b. a -> b
coe T_Sort_156
v2) (T_Sort_156 -> AgdaAny
forall a b. a -> b
coe T_Sort_156
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v2
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v3 T_Abs_112
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v3 T_Abs_112
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((T_Literal_124 -> T_Literal_124 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Literal_124 -> T_Literal_124 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Literal.d__'8799'__48 (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v2)
                       (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v2 [T_Arg_88]
v3
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v4 [T_Arg_88]
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v4 T_Abs_112
v5
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_meta'45'injective_440)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Reflection.AST.Meta.d__'8799'__10 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Args__218 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
        -> case T_Term_154 -> T_Term_154
forall a b. a -> b
coe T_Term_154
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_172 Integer
v2 [T_Arg_88]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_178 AgdaAny
v2 [T_Arg_88]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_def_184 AgdaAny
v2 [T_Arg_88]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lam_190 T_Visibility_48
v2 T_Abs_112
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pat'45'lam_196 [T_Clause_160]
v2 [T_Arg_88]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_pi_202 T_Arg_88
v2 T_Abs_112
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_agda'45'sort_206 T_Sort_156
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_210 T_Literal_124
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_meta_214 AgdaAny
v2 [T_Arg_88]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Term_154
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_216
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Term_154
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Sort_
d__'8799''45'Sort__226 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Sort_156 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Sort_156 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Sort__226 :: T_Sort_156 -> T_Sort_156 -> T_Dec_20
d__'8799''45'Sort__226 T_Sort_156
v0 T_Sort_156
v1
  = case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v2
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v2) (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v2
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v2
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v2) (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v2
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v2
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
        -> case T_Sort_156 -> T_Sort_156
forall a b. a -> b
coe T_Sort_156
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_set_220 T_Term_154
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_224 Integer
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_prop_228 T_Term_154
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_propLit_232 Integer
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_inf_236 Integer
v2
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Sort_156
MAlonzo.Code.Agda.Builtin.Reflection.C_unknown_238
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Sort_156
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Patterns_
d__'8799''45'Patterns__228 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Patterns__228 :: [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Patterns__228 [T_Arg_88]
v0 [T_Arg_88]
v1
  = case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v0 of
      []
        -> case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             (:) AgdaAny
v2 [AgdaAny]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> case AgdaAny -> T_Arg_88
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v4 AgdaAny
v5
               -> case [T_Arg_88] -> [AgdaAny]
forall a b. a -> b
coe [T_Arg_88]
v1 of
                    []
                      -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                           Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                           (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                    (:) AgdaAny
v6 [AgdaAny]
v7
                      -> case AgdaAny -> T_Arg_88
forall a b. a -> b
coe AgdaAny
v6 of
                           MAlonzo.Code.Agda.Builtin.Reflection.C_arg_98 T_ArgInfo_76
v8 AgdaAny
v9
                             -> (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                                  T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Data.List.Properties.du_'8759''45'dec_52
                                  ((T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_Arg_88 -> T_Arg_88 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Argument.du_unArg'45'dec_84
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6)
                                     ((T_Pattern_158 -> T_Pattern_158 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Pattern_158 -> T_Pattern_158 -> T_Dec_20
d__'8799''45'Pattern__230 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
                                  (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Patterns__228 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7))
                           T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Arg_88
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Pattern_
d__'8799''45'Pattern__230 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Pattern_158 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Pattern_158 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Pattern__230 :: T_Pattern_158 -> T_Pattern_158 -> T_Dec_20
d__'8799''45'Pattern__230 T_Pattern_158
v0 T_Pattern_158
v1
  = case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v0 of
      MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v2 [T_Arg_88]
v3
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v4 [T_Arg_88]
v5
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                    ((T__'8801'__12 -> T_Σ_14) -> AgdaAny
forall a b. a -> b
coe T__'8801'__12 -> T_Σ_14
du_pat'45'con'45'injective_1046)
                    ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                       ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Reflection.AST.Name.d__'8799'__12 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                       (([T_Arg_88] -> [T_Arg_88] -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Arg_88] -> [T_Arg_88] -> T_Dec_20
d__'8799''45'Patterns__228 ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v3) ([T_Arg_88] -> AgdaAny
forall a b. a -> b
coe [T_Arg_88]
v5)))
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v2
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased ((T_Term_154 -> T_Term_154 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Term_154 -> T_Term_154 -> T_Dec_20
d__'8799'__224 (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v2) (T_Term_154 -> AgdaAny
forall a b. a -> b
coe T_Term_154
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v2
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v2
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((T_Literal_124 -> T_Literal_124 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Literal_124 -> T_Literal_124 -> T_Dec_20
MAlonzo.Code.Reflection.AST.Literal.d__'8799'__48 (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v2)
                       (T_Literal_124 -> AgdaAny
forall a b. a -> b
coe T_Literal_124
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v2
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((AgdaAny -> AgdaAny -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       AgdaAny -> AgdaAny -> T_Dec_20
MAlonzo.Code.Reflection.AST.Name.d__'8799'__12 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v3))
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v2
        -> case T_Pattern_158 -> T_Pattern_158
forall a b. a -> b
coe T_Pattern_158
v1 of
             MAlonzo.Code.Agda.Builtin.Reflection.C_con_244 AgdaAny
v3 [T_Arg_88]
v4
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_dot_248 T_Term_154
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_var_252 Integer
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_lit_256 T_Literal_124
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_proj_260 AgdaAny
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             MAlonzo.Code.Agda.Builtin.Reflection.C_absurd_264 Integer
v3
               -> ((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                    AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
                    ((Integer -> Integer -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688 (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v2) (Integer -> AgdaAny
forall a b. a -> b
coe Integer
v3))
             T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Pattern_158
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term._≟-Telescope_
d__'8799''45'Telescope__280 ::
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  [MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14] ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d__'8799''45'Telescope__280 :: [T_Σ_14] -> [T_Σ_14] -> T_Dec_20
d__'8799''45'Telescope__280 [T_Σ_14]
v0 [T_Σ_14]
v1
  = case [T_Σ_14] -> [AgdaAny]
forall a b. a -> b
coe [T_Σ_14]
v0 of
      []
        -> case [T_Σ_14] -> [AgdaAny]
forall a b. a -> b
coe [T_Σ_14]
v1 of
             []
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                    ((AgdaAny -> T_Reflects_16) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 AgdaAny
forall a. a
erased)
             (:) AgdaAny
v2 [AgdaAny]
v3
               -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                    Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                    (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                    (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
             [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      (:) AgdaAny
v2 [AgdaAny]
v3
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v4 AgdaAny
v5
               -> case [T_Σ_14] -> [AgdaAny]
forall a b. a -> b
coe [T_Σ_14]
v1 of
                    []
                      -> (Bool -> T_Reflects_16 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                           Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                           (Bool -> AgdaAny
forall a b. a -> b
coe Bool
MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                           (T_Reflects_16 -> AgdaAny
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                    (:) AgdaAny
v6 [AgdaAny]
v7
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v6 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                             -> (T_Dec_20 -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> T_Dec_20
forall a b. a -> b
coe
                                  T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Data.List.Properties.du_'8759''45'dec_52
                                  (((AgdaAny -> AgdaAny)
 -> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20)
-> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (AgdaAny -> AgdaAny)
-> (AgdaAny -> AgdaAny) -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                                     (((AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (AgdaAny -> AgdaAny -> AgdaAny) -> T_Σ_14 -> AgdaAny
MAlonzo.Code.Data.Product.Base.du_uncurry_244 AgdaAny
forall a. a
erased)
                                     (\ AgdaAny
v10 ->
                                        T_Σ_14 -> AgdaAny
forall a b. a -> b
coe
                                          T_Σ_14
MAlonzo.Code.Data.Product.Properties.du_'44''45'injective_142)
                                     ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                                        ((T_String_6 -> T_String_6 -> T_Dec_20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_String_6 -> T_String_6 -> T_Dec_20
MAlonzo.Code.Data.String.Properties.d__'8799'__54
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v8))
                                        ((T_Arg_88 -> T_Arg_88 -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Arg_88 -> T_Arg_88 -> T_Dec_20
d__'8799''45'ArgTerm__214 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9))))
                                  (([T_Σ_14] -> [T_Σ_14] -> T_Dec_20) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe [T_Σ_14] -> [T_Σ_14] -> T_Dec_20
d__'8799''45'Telescope__280 ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v3) ([AgdaAny] -> AgdaAny
forall a b. a -> b
coe [AgdaAny]
v7))
                           T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
                    [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
      [AgdaAny]
_ -> T_Dec_20
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Reflection.AST.Term.var-injective₁
d_var'45'injective'8321'_330 ::
  Integer ->
  Integer ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_var'45'injective'8321'_330 :: Integer
-> Integer
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_var'45'injective'8321'_330 = Integer
-> Integer
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.var-injective₂
d_var'45'injective'8322'_340 ::
  Integer ->
  Integer ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_var'45'injective'8322'_340 :: Integer
-> Integer
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_var'45'injective'8322'_340 = Integer
-> Integer
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.var-injective
d_var'45'injective_350 ::
  Integer ->
  Integer ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_var'45'injective_350 :: Integer
-> Integer -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_var'45'injective_350 ~Integer
v0 ~Integer
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3 = T__'8801'__12 -> T_Σ_14
du_var'45'injective_350
du_var'45'injective_350 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_var'45'injective_350 :: T__'8801'__12 -> T_Σ_14
du_var'45'injective_350
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.con-injective₁
d_con'45'injective'8321'_360 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_con'45'injective'8321'_360 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_con'45'injective'8321'_360 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.con-injective₂
d_con'45'injective'8322'_370 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_con'45'injective'8322'_370 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_con'45'injective'8322'_370 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.con-injective
d_con'45'injective_380 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_con'45'injective_380 :: AgdaAny
-> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_con'45'injective_380 ~AgdaAny
v0 ~AgdaAny
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3 = T__'8801'__12 -> T_Σ_14
du_con'45'injective_380
du_con'45'injective_380 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_con'45'injective_380 :: T__'8801'__12 -> T_Σ_14
du_con'45'injective_380
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.def-injective₁
d_def'45'injective'8321'_390 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_def'45'injective'8321'_390 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_def'45'injective'8321'_390 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.def-injective₂
d_def'45'injective'8322'_400 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_def'45'injective'8322'_400 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_def'45'injective'8322'_400 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.def-injective
d_def'45'injective_410 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_def'45'injective_410 :: AgdaAny
-> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_def'45'injective_410 ~AgdaAny
v0 ~AgdaAny
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3 = T__'8801'__12 -> T_Σ_14
du_def'45'injective_410
du_def'45'injective_410 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_def'45'injective_410 :: T__'8801'__12 -> T_Σ_14
du_def'45'injective_410
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.meta-injective₁
d_meta'45'injective'8321'_420 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_meta'45'injective'8321'_420 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_meta'45'injective'8321'_420 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.meta-injective₂
d_meta'45'injective'8322'_430 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_meta'45'injective'8322'_430 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_meta'45'injective'8322'_430 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.meta-injective
d_meta'45'injective_440 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_meta'45'injective_440 :: AgdaAny
-> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_meta'45'injective_440 ~AgdaAny
v0 ~AgdaAny
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3 = T__'8801'__12 -> T_Σ_14
du_meta'45'injective_440
du_meta'45'injective_440 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_meta'45'injective_440 :: T__'8801'__12 -> T_Σ_14
du_meta'45'injective_440
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.lam-injective₁
d_lam'45'injective'8321'_450 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lam'45'injective'8321'_450 :: T_Visibility_48
-> T_Visibility_48
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
d_lam'45'injective'8321'_450 = T_Visibility_48
-> T_Visibility_48
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.lam-injective₂
d_lam'45'injective'8322'_460 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lam'45'injective'8322'_460 :: T_Visibility_48
-> T_Visibility_48
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
d_lam'45'injective'8322'_460 = T_Visibility_48
-> T_Visibility_48
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.lam-injective
d_lam'45'injective_470 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Visibility_48 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_lam'45'injective_470 :: T_Visibility_48
-> T_Visibility_48
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T_Σ_14
d_lam'45'injective_470 ~T_Visibility_48
v0 ~T_Visibility_48
v1 ~T_Abs_112
v2 ~T_Abs_112
v3 = T__'8801'__12 -> T_Σ_14
du_lam'45'injective_470
du_lam'45'injective_470 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_lam'45'injective_470 :: T__'8801'__12 -> T_Σ_14
du_lam'45'injective_470
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.pat-lam-injective₁
d_pat'45'lam'45'injective'8321'_480 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'lam'45'injective'8321'_480 :: [T_Clause_160]
-> [T_Clause_160]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_pat'45'lam'45'injective'8321'_480 = [T_Clause_160]
-> [T_Clause_160]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-lam-injective₂
d_pat'45'lam'45'injective'8322'_490 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'lam'45'injective'8322'_490 :: [T_Clause_160]
-> [T_Clause_160]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_pat'45'lam'45'injective'8322'_490 = [T_Clause_160]
-> [T_Clause_160]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-lam-injective
d_pat'45'lam'45'injective_500 ::
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Clause_160] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_pat'45'lam'45'injective_500 :: [T_Clause_160]
-> [T_Clause_160]
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T_Σ_14
d_pat'45'lam'45'injective_500 ~[T_Clause_160]
v0 ~[T_Clause_160]
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3
  = T__'8801'__12 -> T_Σ_14
du_pat'45'lam'45'injective_500
du_pat'45'lam'45'injective_500 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_pat'45'lam'45'injective_500 :: T__'8801'__12 -> T_Σ_14
du_pat'45'lam'45'injective_500
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.pi-injective₁
d_pi'45'injective'8321'_510 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pi'45'injective'8321'_510 :: T_Arg_88
-> T_Arg_88
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
d_pi'45'injective'8321'_510 = T_Arg_88
-> T_Arg_88
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pi-injective₂
d_pi'45'injective'8322'_520 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pi'45'injective'8322'_520 :: T_Arg_88
-> T_Arg_88
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
d_pi'45'injective'8322'_520 = T_Arg_88
-> T_Arg_88
-> T_Abs_112
-> T_Abs_112
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pi-injective
d_pi'45'injective_530 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Abs_112 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_pi'45'injective_530 :: T_Arg_88
-> T_Arg_88 -> T_Abs_112 -> T_Abs_112 -> T__'8801'__12 -> T_Σ_14
d_pi'45'injective_530 ~T_Arg_88
v0 ~T_Arg_88
v1 ~T_Abs_112
v2 ~T_Abs_112
v3 = T__'8801'__12 -> T_Σ_14
du_pi'45'injective_530
du_pi'45'injective_530 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_pi'45'injective_530 :: T__'8801'__12 -> T_Σ_14
du_pi'45'injective_530
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.sort-injective
d_sort'45'injective_536 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Sort_156 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Sort_156 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sort'45'injective_536 :: T_Sort_156 -> T_Sort_156 -> T__'8801'__12 -> T__'8801'__12
d_sort'45'injective_536 = T_Sort_156 -> T_Sort_156 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.lit-injective
d_lit'45'injective_542 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Literal_124 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Literal_124 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_lit'45'injective_542 :: T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12
d_lit'45'injective_542 = T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.set-injective
d_set'45'injective_548 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_set'45'injective_548 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
d_set'45'injective_548 = T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.slit-injective
d_slit'45'injective_554 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_slit'45'injective_554 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_slit'45'injective_554 = Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.prop-injective
d_prop'45'injective_560 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_prop'45'injective_560 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
d_prop'45'injective_560 = T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.propLit-injective
d_propLit'45'injective_566 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_propLit'45'injective_566 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_propLit'45'injective_566 = Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.inf-injective
d_inf'45'injective_572 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_inf'45'injective_572 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_inf'45'injective_572 = Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-con-injective₁
d_pat'45'con'45'injective'8321'_1026 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'con'45'injective'8321'_1026 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_pat'45'con'45'injective'8321'_1026 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-con-injective₂
d_pat'45'con'45'injective'8322'_1036 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'con'45'injective'8322'_1036 :: AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
d_pat'45'con'45'injective'8322'_1036 = AgdaAny
-> AgdaAny
-> [T_Arg_88]
-> [T_Arg_88]
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-con-injective
d_pat'45'con'45'injective_1046 ::
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  [MAlonzo.Code.Agda.Builtin.Reflection.T_Arg_88] ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
d_pat'45'con'45'injective_1046 :: AgdaAny
-> AgdaAny -> [T_Arg_88] -> [T_Arg_88] -> T__'8801'__12 -> T_Σ_14
d_pat'45'con'45'injective_1046 ~AgdaAny
v0 ~AgdaAny
v1 ~[T_Arg_88]
v2 ~[T_Arg_88]
v3
  = T__'8801'__12 -> T_Σ_14
du_pat'45'con'45'injective_1046
du_pat'45'con'45'injective_1046 ::
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
du_pat'45'con'45'injective_1046 :: T__'8801'__12 -> T_Σ_14
du_pat'45'con'45'injective_1046
  = ((AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14)
-> AgdaAny -> AgdaAny -> T__'8801'__12 -> T_Σ_14
forall a b. a -> b
coe
      (AgdaAny -> AgdaAny) -> (AgdaAny -> AgdaAny) -> AgdaAny -> T_Σ_14
MAlonzo.Code.Data.Product.Base.du_'60'_'44'_'62'_112 AgdaAny
forall a. a
erased AgdaAny
forall a. a
erased
-- Reflection.AST.Term.pat-var-injective
d_pat'45'var'45'injective_1052 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'var'45'injective_1052 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_pat'45'var'45'injective_1052 = Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.pat-lit-injective
d_pat'45'lit'45'injective_1058 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Literal_124 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Literal_124 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_pat'45'lit'45'injective_1058 :: T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12
d_pat'45'lit'45'injective_1058 = T_Literal_124 -> T_Literal_124 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.proj-injective
d_proj'45'injective_1064 ::
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_proj'45'injective_1064 :: AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
d_proj'45'injective_1064 = AgdaAny -> AgdaAny -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.dot-injective
d_dot'45'injective_1070 ::
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Reflection.T_Term_154 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_dot'45'injective_1070 :: T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
d_dot'45'injective_1070 = T_Term_154 -> T_Term_154 -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased
-- Reflection.AST.Term.absurd-injective
d_absurd'45'injective_1076 ::
  Integer ->
  Integer ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_absurd'45'injective_1076 :: Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
d_absurd'45'injective_1076 = Integer -> Integer -> T__'8801'__12 -> T__'8801'__12
forall a. a
erased