{-# 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.Type.BetaNBE.Soundness where

import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                    quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                    rem64, lt64, eq64, word64FromNat, word64ToNat)
import qualified MAlonzo.RTE
import qualified Data.Text
import qualified MAlonzo.Code.Agda.Builtin.Equality
import qualified MAlonzo.Code.Agda.Builtin.Sigma
import qualified MAlonzo.Code.Data.Sum.Base
import qualified MAlonzo.Code.Data.Vec.Base
import qualified MAlonzo.Code.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.BetaNormal
import qualified MAlonzo.Code.Type.Equality
import qualified MAlonzo.Code.Type.RenamingSubstitution
import qualified MAlonzo.Code.Utils

-- Type.BetaNBE.Soundness.SR
d_SR_10 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 -> AgdaAny -> ()
d_SR_10 :: T_Ctx'8902'_2 -> T_Kind_476 -> T__'8866''8902'__20 -> AgdaAny -> ()
d_SR_10 = T_Ctx'8902'_2 -> T_Kind_476 -> T__'8866''8902'__20 -> AgdaAny -> ()
forall a. a
erased
-- Type.BetaNBE.Soundness.reflectSR
d_reflectSR_54 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
  MAlonzo.Code.Type.Equality.T__'8801'β__10 -> AgdaAny
d_reflectSR_54 :: T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866'Ne'8902'__6
-> T__'8801'β__10
-> AgdaAny
d_reflectSR_54 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 ~T__'8866''8902'__20
v2 ~T__'8866'Ne'8902'__6
v3 T__'8801'β__10
v4 = T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 T_Kind_476
v1 T__'8801'β__10
v4
du_reflectSR_54 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.Equality.T__'8801'β__10 -> AgdaAny
du_reflectSR_54 :: T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 T_Kind_476
v0 T__'8801'β__10
v1 = (AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b -> b
seq (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0) (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
v1)
-- Type.BetaNBE.Soundness.reifySR
d_reifySR_74 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Type.Equality.T__'8801'β__10
d_reifySR_74 :: T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> T__'8801'β__10
d_reifySR_74 T_Ctx'8902'_2
v0 T_Kind_476
v1 ~T__'8866''8902'__20
v2 AgdaAny
v3 AgdaAny
v4 = T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 T_Ctx'8902'_2
v0 T_Kind_476
v1 AgdaAny
v3 AgdaAny
v4
du_reifySR_74 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  AgdaAny -> AgdaAny -> MAlonzo.Code.Type.Equality.T__'8801'β__10
du_reifySR_74 :: T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 T_Ctx'8902'_2
v0 T_Kind_476
v1 AgdaAny
v2 AgdaAny
v3
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v1 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478 -> AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v3
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480 -> AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v3
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v4 T_Kind_476
v5
        -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v2 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v6 -> AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v3
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v6
               -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v3 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v7 AgdaAny
v8
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v8 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v9 AgdaAny
v10
                             -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe
                                  T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                                  ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28 AgdaAny
v7) AgdaAny
v9
                                  ((T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                                     ((T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
                                        T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                        (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346
                                           ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                              T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                              ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                              (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                           ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                              T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                           (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T__'8866''8902'__20
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
forall a b. a -> b
coe
                                              (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8866''8902'__20
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_sub'45'cons_420
                                              (\ AgdaAny
v11 AgdaAny
v12 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 AgdaAny
v12)
                                              ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                                 (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))
                                           (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v5)
                                           ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8866''8902'__20
forall a b. a -> b
coe
                                              T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                              ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                              ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                                 ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                    (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                              (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18
                                                 ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v11 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)))
                                              (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v5) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7))))
                                     (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76)
                                     ((T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                        T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_ƛ'8801'β_24
                                        ((T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                                           ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v4
                                              ((T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
                                                 T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                                 (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                                    ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                                       T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                       (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                    ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                                       T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                          T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                                          (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                       (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                    (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8715''8902'__14
forall a b. a -> b
coe
                                                       (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18
                                                       ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                                          (\ AgdaAny
v11 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)))
                                                    (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v5) (AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe AgdaAny
v7)))
                                              ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                                 (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))
                                           ((T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_sym'8801'β_16
                                              (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_β'8801'β_48))
                                           ((T_Ctx'8902'_2
 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74
                                              ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                              (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v5)
                                              (AgdaAny -> AgdaAny -> (AgdaAny -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny
v6
                                                 ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                    (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                 (\ AgdaAny
v11 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)
                                                 ((T_Kind_476 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Kind_476 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du_fresh_38 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4)))
                                              (AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                 AgdaAny
v10
                                                 ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                    (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                                                 (\ AgdaAny
v11 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)
                                                 ((T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22
                                                    (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16))
                                                 ((T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Kind_476 -> T__'8866'Ne'8902'__6 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du_reflect_22 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4)
                                                    ((T__'8715''8902'__14 -> T__'8866'Ne'8902'__6) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                       T__'8715''8902'__14 -> T__'8866'Ne'8902'__6
MAlonzo.Code.Type.BetaNormal.C_'96'_8
                                                       (T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16)))
                                                 ((T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                    T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4)
                                                    (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe
                                                       T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14)))))))
                           T_Σ_14
_ -> T__'8801'β__10
forall a. a
MAlonzo.RTE.mazUnreachableError
                    T_Σ_14
_ -> T__'8801'β__10
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> T__'8801'β__10
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Kind_476
_ -> T__'8801'β__10
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.SREnv
d_SREnv_108 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  ()
d_SREnv_108 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> ()
d_SREnv_108 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> ()
forall a. a
erased
-- Type.BetaNBE.Soundness.SR,,⋆
d_SR'44''44''8902'_134 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_SR'44''44''8902'_134 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
d_SR'44''44''8902'_134 ~T_Ctx'8902'_2
v0 ~T_Ctx'8902'_2
v1 ~T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v2 ~T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 ~T_Kind_476
v5 ~T__'8866''8902'__20
v6 ~AgdaAny
v7 AgdaAny
v8 T_Kind_476
v9 T__'8715''8902'__14
v10
  = (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_SR'44''44''8902'_134 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 AgdaAny
v8 T_Kind_476
v9 T__'8715''8902'__14
v10
du_SR'44''44''8902'_134 ::
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  AgdaAny ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du_SR'44''44''8902'_134 :: (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_SR'44''44''8902'_134 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 AgdaAny
v1 T_Kind_476
v2 T__'8715''8902'__14
v3
  = case T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T__'8715''8902'__14
v3 of
      T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v1
      MAlonzo.Code.Type.C_S_18 T__'8715''8902'__14
v7 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 T_Kind_476
v2 T__'8715''8902'__14
v7
      T__'8715''8902'__14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.subSR
d_subSR_156 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.Equality.T__'8801'β__10 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_subSR_156 :: T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_subSR_156 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866''8902'__20
v2 ~T__'8866''8902'__20
v3 T__'8801'β__10
v4 AgdaAny
v5 AgdaAny
v6 = T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subSR_156 T_Kind_476
v1 T__'8866''8902'__20
v2 T__'8801'β__10
v4 AgdaAny
v5 AgdaAny
v6
du_subSR_156 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.Equality.T__'8801'β__10 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_subSR_156 :: T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subSR_156 T_Kind_476
v0 T__'8866''8902'__20
v1 T__'8801'β__10
v2 AgdaAny
v3 AgdaAny
v4
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v0 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478
        -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18 T__'8866''8902'__20
v1 T__'8801'β__10
v2 AgdaAny
v4
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480
        -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18 T__'8866''8902'__20
v1 T__'8801'β__10
v2 AgdaAny
v4
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v5 T_Kind_476
v6
        -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v3 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v7
               -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18 T__'8866''8902'__20
v1 T__'8801'β__10
v2 AgdaAny
v4
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v7
               -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v4 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v8 AgdaAny
v9
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v9 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                             -> (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
v8)
                                  ((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__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18 T__'8866''8902'__20
v1 T__'8801'β__10
v2 AgdaAny
v10)
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v11))
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.renSR
d_renSR_202 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_renSR_202 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_renSR_202 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 T_Kind_476
v3 T__'8866''8902'__20
v4 AgdaAny
v5 AgdaAny
v6
  = case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3 of
      T_Kind_476
MAlonzo.Code.Utils.C_'42'_478
        -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3)
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'β__10
-> T__'8801'β__10
MAlonzo.Code.Type.Equality.d_ren'8801'β_80
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v4)
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v6))
             ((T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_sym'8801'β_16
                (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76))
      T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480
        -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3)
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5)))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'β__10
-> T__'8801'β__10
MAlonzo.Code.Type.Equality.d_ren'8801'β_80
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v4)
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.d_embNf_128 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v6))
             ((T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_sym'8801'β_16
                (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76))
      MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v7 T_Kind_476
v8
        -> case AgdaAny -> T__'8846'__30
forall a b. a -> b
coe AgdaAny
v5 of
             MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v9
               -> (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> T__'8801'β__10 -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                    T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                    (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                       (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3)
                       ((T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.du_embNe_134 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9)))
                    (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'β__10
-> T__'8801'β__10
MAlonzo.Code.Type.Equality.d_ren'8801'β_80
                       (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v3) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v4)
                       ((T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8866''8902'__20
MAlonzo.Code.Type.BetaNormal.du_embNe_134 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v9))
                       ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe AgdaAny
v6))
                    ((T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_sym'8801'β_16
                       (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76))
             MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v9
               -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v6 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v10 AgdaAny
v11
                      -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v11 of
                           MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v12 AgdaAny
v13
                             -> (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_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                     ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v7))
                                     ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v7))
                                     (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2))
                                     (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v10))
                                  ((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_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T__'8801'β__10
 -> T__'8801'β__10)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                        T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8801'β__10
-> T__'8801'β__10
MAlonzo.Code.Type.Equality.d_ren'8801'β_80 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                                        (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v4) ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28 AgdaAny
v10)
                                        ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v12))
                                     ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 AgdaAny
v18 ->
                                           (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8801'β__10
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                             T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subSR_156 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                                             ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v7
                                                ((T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
                                                   T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                                   (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                                      ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                                         T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v7))
                                                      ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe
                                                         T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6
                                                         (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v7))
                                                      (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8715''8902'__14
forall a b. a -> b
coe
                                                         (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18
                                                         ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                                            (\ AgdaAny
v19 ->
                                                               let v20 :: t
v20 = (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> t
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 AgdaAny
v19 in
                                                               (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                                                 (\ AgdaAny
v21 ->
                                                                    AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15 AgdaAny
v19 (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v20 AgdaAny
v21)))))
                                                      (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v8) (AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe AgdaAny
v10)))
                                                AgdaAny
v16)
                                             (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76)
                                             ((T_Ctx'8902'_2
 -> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny
MAlonzo.Code.Type.BetaNBE.d__'183'V__150 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                                (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v7) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                                                ((T_Kind_476
 -> T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                                   T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_renVal_46 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v3)
                                                   (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14)
                                                   ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v19 AgdaAny
v20 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15 AgdaAny
v19 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 AgdaAny
v19 AgdaAny
v20)))
                                                   (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v5))
                                                (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17))
                                             (AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                                AgdaAny
v13 AgdaAny
v14 (\ AgdaAny
v19 AgdaAny
v20 -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15 AgdaAny
v19 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
v2 AgdaAny
v19 AgdaAny
v20))
                                                AgdaAny
v16 AgdaAny
v17 AgdaAny
v18))))
                           T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.exts-sub-cons
d_exts'45'sub'45'cons_268 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_exts'45'sub'45'cons_268 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8715''8902'__14
-> T__'8801'__12
d_exts'45'sub'45'cons_268 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8715''8902'__14
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.Soundness.subSREnv
d_subSREnv_288 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_subSREnv_288 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8801'__12)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
d_subSREnv_288 ~T_Ctx'8902'_2
v0 ~T_Ctx'8902'_2
v1 ~T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v2 ~T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3 ~T_Kind_476 -> T__'8715''8902'__14 -> T__'8801'__12
v4 ~T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6 T_Kind_476
v7 T__'8715''8902'__14
v8
  = (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_subSREnv_288 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6 T_Kind_476
v7 T__'8715''8902'__14
v8
du_subSREnv_288 ::
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du_subSREnv_288 :: (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_subSREnv_288 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 T_Kind_476
v1 T__'8715''8902'__14
v2 = (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v0 T_Kind_476
v1 T__'8715''8902'__14
v2
-- Type.BetaNBE.Soundness.SRweak
d_SRweak_310 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_SRweak_310 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
d_SRweak_310 ~T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476
v5 T_Kind_476
v6
  = T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_SRweak_310 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476
v5 T_Kind_476
v6
du_SRweak_310 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
du_SRweak_310 :: T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_SRweak_310 T_Ctx'8902'_2
v0 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v1 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476
v4 T_Kind_476
v5
  = ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe
      (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_subSREnv_288
      (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_SR'44''44''8902'_134
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v6 AgdaAny
v7 ->
               T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_renSR_202
                 (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4))
                 ((AgdaAny -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe (\ AgdaAny
v8 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)) (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v6)
                 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v1 AgdaAny
v6 AgdaAny
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v2 AgdaAny
v6 AgdaAny
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 AgdaAny
v6 AgdaAny
v7)))
         ((T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v4)
            (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14)))
      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v5)
-- Type.BetaNBE.Soundness.SRApp
d_SRApp_328 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  AgdaAny ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  AgdaAny -> AgdaAny -> AgdaAny
d_SRApp_328 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8846'__30
-> AgdaAny
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_SRApp_328 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2 ~T__'8866''8902'__20
v3 T__'8846'__30
v4 AgdaAny
v5 T__'8866''8902'__20
v6 AgdaAny
v7 AgdaAny
v8
  = T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8846'__30
-> AgdaAny
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_SRApp_328 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2 T__'8846'__30
v4 AgdaAny
v5 T__'8866''8902'__20
v6 AgdaAny
v7 AgdaAny
v8
du_SRApp_328 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Data.Sum.Base.T__'8846'__30 ->
  AgdaAny ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  AgdaAny -> AgdaAny -> AgdaAny
du_SRApp_328 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8846'__30
-> AgdaAny
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_SRApp_328 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2 T__'8846'__30
v3 AgdaAny
v4 T__'8866''8902'__20
v5 AgdaAny
v6 AgdaAny
v7
  = case T__'8846'__30 -> T__'8846'__30
forall a b. a -> b
coe T__'8846'__30
v3 of
      MAlonzo.Code.Data.Sum.Base.C_inj'8321'_38 AgdaAny
v8
        -> (T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             ((T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_'183''8801'β_26
                ((T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v4))
                ((T_Ctx'8902'_2
 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6) (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v7)))
      MAlonzo.Code.Data.Sum.Base.C_inj'8322'_42 AgdaAny
v8
        -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v4 of
             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v9 AgdaAny
v10
               -> case AgdaAny -> T_Σ_14
forall a b. a -> b
coe AgdaAny
v10 of
                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 AgdaAny
v11 AgdaAny
v12
                      -> (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8801'β__10
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                           T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subSR_156 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
                           ((T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> T_Kind_476 -> AgdaAny -> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
                              T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v1
                              ((T__'8866''8902'__20 -> T__'8866''8902'__20)
-> T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe
                                 T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28
                                 (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                    ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1))
                                    ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1))
                                    (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8715''8902'__14
forall a b. a -> b
coe
                                       (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18
                                       ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v13 AgdaAny
v14 -> AgdaAny
v14)))
                                    (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v2) (AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe AgdaAny
v9)))
                              T__'8866''8902'__20
v5)
                           ((T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_'183''8801'β_26
                              ((T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                                 ((T__'8866''8902'__20 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_ƛ_28 AgdaAny
v9) AgdaAny
v11
                                 (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76))
                              (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14))
                           ((T_Ctx'8902'_2
 -> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                              T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8846'__30 -> AgdaAny -> AgdaAny
MAlonzo.Code.Type.BetaNBE.d__'183'V__150 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
                              ((T_Kind_476
 -> T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                 T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_renVal_46
                                 ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                                 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe (\ AgdaAny
v13 AgdaAny
v14 -> AgdaAny
v14)) (T__'8846'__30 -> AgdaAny
forall a b. a -> b
coe T__'8846'__30
v3))
                              (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v6))
                           (AgdaAny
-> T_Ctx'8902'_2
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe AgdaAny
v12 T_Ctx'8902'_2
v0 (\ AgdaAny
v13 AgdaAny
v14 -> AgdaAny
v14) T__'8866''8902'__20
v5 AgdaAny
v6 AgdaAny
v7)
                    T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
             T_Σ_14
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      T__'8846'__30
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.evalSR
d_evalSR_358 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  AgdaAny
d_evalSR_358 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T__'8866''8902'__20
v3 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6
  = case T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v3 of
      MAlonzo.Code.Type.C_'96'_22 T__'8715''8902'__14
v9 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6 T_Kind_476
v2 T__'8715''8902'__14
v9
      MAlonzo.Code.Type.C_Π_24 T_Kind_476
v8 T__'8866''8902'__20
v9
        -> (T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_Π'8801'β_22
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8))
                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8))
                (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v9)
                ((T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_exts_336 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                   ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8))
                (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
forall a b. a -> b
coe
                   (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du__'44''44''8902'__122
                   ((AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                      (\ AgdaAny
v10 ->
                         let v11 :: t
v11 = (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny -> t
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 AgdaAny
v10 in
                         (AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                           (\ AgdaAny
v12 ->
                              T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_renVal_46
                                (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v10) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                                ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8))
                                ((AgdaAny -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe (\ AgdaAny
v13 -> (T__'8715''8902'__14 -> T__'8715''8902'__14) -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.C_S_18)) (AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
forall a. a
v11 AgdaAny
v12))))
                   ((T_Kind_476 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du_fresh_38 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)))
                ((T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> AgdaAny
du_SRweak_310 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)))
      MAlonzo.Code.Type.C__'8658'__26 T__'8866''8902'__20
v8 T__'8866''8902'__20
v9
        -> (T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_'8658''8801'β_20
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v8)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v9)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
      MAlonzo.Code.Type.C_ƛ_28 T__'8866''8902'__20
v10
        -> case T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v2 of
             MAlonzo.Code.Utils.C__'8658'__482 T_Kind_476
v11 T_Kind_476
v12
               -> (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_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                       T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                       ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                       ((T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                          T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_exts_336 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                          ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                       (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10))
                    ((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__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14)
                       ((AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
                          (\ AgdaAny
v13 AgdaAny
v14 AgdaAny
v15 AgdaAny
v16 AgdaAny
v17 ->
                             (T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8801'β__10
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                               T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_subSR_156 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12)
                               ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346
                                  ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                  (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T__'8866''8902'__20
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8866''8902'__20
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_sub'45'cons_420
                                     ((AgdaAny -> AgdaAny -> T__'8866''8902'__20) -> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v18 AgdaAny
v19 ->
                                           T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                             (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v14) (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v18)
                                             ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 AgdaAny
v18 AgdaAny
v19)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))
                                  (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10))
                               ((T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
                                  (T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d__'91'_'93'_432
                                     (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v11) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v12)
                                     ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8866''8902'__20
forall a b. a -> b
coe
                                        T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                        ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                        ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                        (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
 -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
MAlonzo.Code.Type.RenamingSubstitution.du_ext_18
                                           (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v14))
                                        (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12)
                                        ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                           T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346
                                           ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                           ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                           ((T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                              T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_exts_336
                                              (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                           (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10)))
                                     (AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe AgdaAny
v15))
                                  (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_β'8801'β_48)
                                  (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76))
                               ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                  T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13)
                                  ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                  (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10)
                                  (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du__'44''44''8902'__122
                                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v18 AgdaAny
v19 ->
                                           T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_renVal_46
                                             (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v18) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v14)
                                             ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 AgdaAny
v18 AgdaAny
v19)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16)))
                               ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                                  T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                                  ((T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2 -> T_Kind_476 -> T_Ctx'8902'_2
MAlonzo.Code.Type.C__'44''8902'__6 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v11))
                                  (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v13) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v12) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10)
                                  (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T__'8866''8902'__20
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8866''8902'__20
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.du_sub'45'cons_420
                                     ((AgdaAny -> AgdaAny -> T__'8866''8902'__20) -> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v18 AgdaAny
v19 ->
                                           T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_ren_28
                                             (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v14) (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v18)
                                             ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 AgdaAny
v18 AgdaAny
v19)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v15))
                                  (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du__'44''44''8902'__122
                                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v18 AgdaAny
v19 ->
                                           T_Kind_476
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> AgdaAny
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_renVal_46
                                             (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v18) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v14)
                                             ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 AgdaAny
v18 AgdaAny
v19)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v16))
                                  (((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                                     (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
du_SR'44''44''8902'_134
                                     ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
                                        (\ AgdaAny
v18 AgdaAny
v19 ->
                                           T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
d_renSR_202
                                             (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Ctx'8902'_2
forall a b. a -> b
coe AgdaAny
v13) (AgdaAny -> T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe AgdaAny
v14) (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v18) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 AgdaAny
v18 AgdaAny
v19)
                                             ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 AgdaAny
v18 AgdaAny
v19) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6 AgdaAny
v18 AgdaAny
v19)))
                                     (AgdaAny -> AgdaAny
forall a b. a -> b
coe AgdaAny
v17))))))
             T_Kind_476
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
      MAlonzo.Code.Type.C__'183'__30 T_Kind_476
v8 T__'8866''8902'__20
v10 T__'8866''8902'__20
v11
        -> (T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8846'__30
 -> AgdaAny
 -> T__'8866''8902'__20
 -> AgdaAny
 -> AgdaAny
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8846'__30
-> AgdaAny
-> T__'8866''8902'__20
-> AgdaAny
-> AgdaAny
-> AgdaAny
du_SRApp_328 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v11))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v11) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v11) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
      MAlonzo.Code.Type.C_μ_32 T_Kind_476
v8 T__'8866''8902'__20
v9 T__'8866''8902'__20
v10
        -> (T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_μ'8801'β_28
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v9) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1)
                   ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                      T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482
                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478))
                      ((T_Kind_476 -> T_Kind_476 -> T_Kind_476)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                         T_Kind_476 -> T_Kind_476 -> T_Kind_476
MAlonzo.Code.Utils.C__'8658'__482 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                         (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478)))
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v9) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6)))
             ((T_Ctx'8902'_2
 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8)
                   (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
                ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                   T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v8) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v10) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5)
                   ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6)))
      MAlonzo.Code.Type.C_'94'_34 T_TyCon_6
v9
        -> (T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v2)
             (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14)
      MAlonzo.Code.Type.C_con_36 T__'8866''8902'__20
v8
        -> (T__'8801'β__10 -> T__'8801'β__10) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_con'8801'β_34
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'9839'_480) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v8)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
      MAlonzo.Code.Type.C_SOP_40 Integer
v8 T_Vec_28
v9
        -> (T__'10216''91''8801''93''10217'β__8 -> T__'8801'β__10)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
             T__'10216''91''8801''93''10217'β__8 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_SOP'8801'β_42
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Vec_28
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T__'10216''91''8801''93''10217'β__8)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'10216''91''8801''93''10217'β__8
du_evalSR'45'VecList_384 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v9) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6))
      T__'8866''8902'__20
_ -> AgdaAny
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.evalSR-List
d_evalSR'45'List_370 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  [MAlonzo.Code.Type.T__'8866''8902'__20] ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Type.Equality.T__'91''8801''93'β__4
d_evalSR'45'List_370 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'91''8801''93'β__4
d_evalSR'45'List_370 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 [T__'8866''8902'__20]
v2 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5
  = case [T__'8866''8902'__20] -> [AgdaAny]
forall a b. a -> b
coe [T__'8866''8902'__20]
v2 of
      [] -> T__'91''8801''93'β__4 -> T__'91''8801''93'β__4
forall a b. a -> b
coe T__'91''8801''93'β__4
MAlonzo.Code.Type.Equality.C_nil'91''8801''93'β_50
      (:) AgdaAny
v6 [AgdaAny]
v7
        -> (T__'8801'β__10 -> T__'91''8801''93'β__4 -> T__'91''8801''93'β__4)
-> AgdaAny -> T__'91''8801''93'β__4 -> T__'91''8801''93'β__4
forall a b. a -> b
coe
             T__'8801'β__10 -> T__'91''8801''93'β__4 -> T__'91''8801''93'β__4
MAlonzo.Code.Type.Equality.C_cons'91''8801''93'β_60
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
MAlonzo.Code.Utils.C_'42'_478) (AgdaAny -> T__'8866''8902'__20
forall a b. a -> b
coe AgdaAny
v6)
                ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'91''8801''93'β__4
d_evalSR'45'List_370
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) ([AgdaAny] -> [T__'8866''8902'__20]
forall a b. a -> b
coe [AgdaAny]
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
      [AgdaAny]
_ -> T__'91''8801''93'β__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.evalSR-VecList
d_evalSR'45'VecList_384 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  Integer ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Type.Equality.T__'10216''91''8801''93''10217'β__8
d_evalSR'45'VecList_384 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> Integer
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'10216''91''8801''93''10217'β__8
d_evalSR'45'VecList_384 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 ~Integer
v2 T_Vec_28
v3 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6
  = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'10216''91''8801''93''10217'β__8
du_evalSR'45'VecList_384 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Vec_28
v3 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v6
du_evalSR'45'VecList_384 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8866''8902'__20) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny) ->
  MAlonzo.Code.Type.Equality.T__'10216''91''8801''93''10217'β__8
du_evalSR'45'VecList_384 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'10216''91''8801''93''10217'β__8
du_evalSR'45'VecList_384 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Vec_28
v2 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5
  = case T_Vec_28 -> T_Vec_28
forall a b. a -> b
coe T_Vec_28
v2 of
      T_Vec_28
MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
        -> T__'10216''91''8801''93''10217'β__8
-> T__'10216''91''8801''93''10217'β__8
forall a b. a -> b
coe
             T__'10216''91''8801''93''10217'β__8
MAlonzo.Code.Type.Equality.C_nil'10216''91''8801''93''10217'β_62
      MAlonzo.Code.Data.Vec.Base.C__'8759'__38 AgdaAny
v7 T_Vec_28
v8
        -> (T__'91''8801''93'β__4
 -> T__'10216''91''8801''93''10217'β__8
 -> T__'10216''91''8801''93''10217'β__8)
-> T__'91''8801''93'β__4
-> AgdaAny
-> T__'10216''91''8801''93''10217'β__8
forall a b. a -> b
coe
             T__'91''8801''93'β__4
-> T__'10216''91''8801''93''10217'β__8
-> T__'10216''91''8801''93''10217'β__8
MAlonzo.Code.Type.Equality.C_cons'10216''91''8801''93''10217'β_74
             (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> [T__'8866''8902'__20]
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'91''8801''93'β__4
d_evalSR'45'List_370
                (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> [T__'8866''8902'__20]
forall a b. a -> b
coe AgdaAny
v7) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
             ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Vec_28
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T__'10216''91''8801''93''10217'β__8)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
forall a b. a -> b
coe
                T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Vec_28
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'10216''91''8801''93''10217'β__8
du_evalSR'45'VecList_384 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (T_Vec_28 -> AgdaAny
forall a b. a -> b
coe T_Vec_28
v8) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20
v3)
                ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5))
      T_Vec_28
_ -> T__'10216''91''8801''93''10217'β__8
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.Soundness.idSR
d_idSR_462 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 -> AgdaAny
d_idSR_462 :: T_Ctx'8902'_2 -> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
d_idSR_462 ~T_Ctx'8902'_2
v0 T_Kind_476
v1 ~T__'8715''8902'__14
v2 = T_Kind_476 -> AgdaAny
du_idSR_462 T_Kind_476
v1
du_idSR_462 :: MAlonzo.Code.Utils.T_Kind_476 -> AgdaAny
du_idSR_462 :: T_Kind_476 -> AgdaAny
du_idSR_462 T_Kind_476
v0
  = (T_Kind_476 -> T__'8801'β__10 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
      T_Kind_476 -> T__'8801'β__10 -> AgdaAny
du_reflectSR_54 (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v0)
      (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.C_refl'8801'β_14)
-- Type.BetaNBE.Soundness.soundness
d_soundness_470 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.Equality.T__'8801'β__10
d_soundness_470 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8801'β__10
d_soundness_470 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866''8902'__20
v2
  = (T__'8866''8902'__20
 -> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10)
-> T__'8866''8902'__20 -> AgdaAny -> AgdaAny -> T__'8801'β__10
forall a b. a -> b
coe
      T__'8866''8902'__20
-> T__'8801'β__10 -> T__'8801'β__10 -> T__'8801'β__10
MAlonzo.Code.Type.Equality.C_trans'8801'β_18
      (T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8866''8902'__20
MAlonzo.Code.Type.RenamingSubstitution.d_sub_346
         (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (\ T_Kind_476
v3 T__'8715''8902'__14
v4 -> (T__'8715''8902'__14 -> T__'8866''8902'__20)
-> T__'8715''8902'__14 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 T__'8715''8902'__14
v4)
         (T_Kind_476 -> T_Kind_476
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866''8902'__20 -> T__'8866''8902'__20
forall a b. a -> b
coe T__'8866''8902'__20
v2))
      (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76)
      ((T_Ctx'8902'_2
 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         T_Ctx'8902'_2 -> T_Kind_476 -> AgdaAny -> AgdaAny -> T__'8801'β__10
du_reifySR_74 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1)
         ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
            T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.d_eval_166 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1)
            (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du_idEnv_250))
         ((T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> T__'8866''8902'__20
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> AgdaAny)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
-> (AgdaAny -> AgdaAny -> AgdaAny)
-> AgdaAny
forall a b. a -> b
coe
            T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866''8902'__20
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866''8902'__20)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> AgdaAny
d_evalSR_358 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v2)
            (\ AgdaAny
v3 AgdaAny
v4 -> (T__'8715''8902'__14 -> T__'8866''8902'__20) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T__'8715''8902'__14 -> T__'8866''8902'__20
MAlonzo.Code.Type.C_'96'_22 AgdaAny
v4)
            ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
MAlonzo.Code.Type.BetaNBE.du_idEnv_250)
            (\ AgdaAny
v3 AgdaAny
v4 -> (T_Kind_476 -> AgdaAny) -> AgdaAny -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> AgdaAny
du_idSR_462 AgdaAny
v3)))