{-# 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.RenamingSubstitution 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.Type
import qualified MAlonzo.Code.Type.BetaNBE
import qualified MAlonzo.Code.Type.BetaNBE.Completeness
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.RenamingSubstitution.reify-reflect
d_reify'45'reflect_12 ::
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_reify'45'reflect_12 :: T_Kind_476
-> T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8801'__12
d_reify'45'reflect_12 = T_Kind_476
-> T_Ctx'8902'_2 -> T__'8866'Ne'8902'__6 -> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.evalCRSubst
d_evalCRSubst_38 ::
  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.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) ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 -> AgdaAny
d_evalCRSubst_38 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'__12
-> AgdaAny
d_evalCRSubst_38 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T__'8866''8902'__20
v6 T__'8866''8902'__20
v7 ~T__'8801'__12
v8
  = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> AgdaAny
du_evalCRSubst_38 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T__'8866''8902'__20
v6 T__'8866''8902'__20
v7
du_evalCRSubst_38 ::
  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.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) ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 -> AgdaAny
du_evalCRSubst_38 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> AgdaAny
du_evalCRSubst_38 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476
v2 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v3 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v4 T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
v5 T__'8866''8902'__20
v6 T__'8866''8902'__20
v7
  = (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> T_Kind_476
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
 -> T__'8866''8902'__20
 -> T__'8866''8902'__20
 -> T__'8801'β__10
 -> 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_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> (T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny)
-> T__'8866''8902'__20
-> T__'8866''8902'__20
-> T__'8801'β__10
-> AgdaAny
MAlonzo.Code.Type.BetaNBE.Completeness.d_fund_1482 (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
v2) ((T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
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__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v6) (T__'8866''8902'__20 -> AgdaAny
forall a b. a -> b
coe T__'8866''8902'__20
v7)
      (T__'8801'β__10 -> AgdaAny
forall a b. a -> b
coe T__'8801'β__10
MAlonzo.Code.Type.Equality.du_'8801'2β_76)
-- Type.BetaNBE.RenamingSubstitution.ren-nf
d_ren'45'nf_56 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'nf_56 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866''8902'__20
-> T__'8801'__12
d_ren'45'nf_56 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866''8902'__20
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.ren-nf-μ
d_ren'45'nf'45'μ_74 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'45'nf'45'μ_74 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_ren'45'nf'45'μ_74 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.SubNf
d_SubNf_90 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 -> ()
d_SubNf_90 :: T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
d_SubNf_90 = T_Ctx'8902'_2 -> T_Ctx'8902'_2 -> ()
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf
d_subNf_104 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_subNf_104 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_subNf_104 T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 T_Kind_476
v3 T__'8866'Nf'8902'__4
v4
  = (T_Ctx'8902'_2
 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866''8902'__20 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNBE.d_nf_258 (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_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)
         ((AgdaAny -> AgdaAny -> T__'8866''8902'__20) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v5 AgdaAny
v6 ->
               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 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v1) (AgdaAny -> T_Kind_476
forall a b. a -> b
coe AgdaAny
v5) ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 AgdaAny
v5 AgdaAny
v6)))
         (T_Kind_476 -> AgdaAny
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 -> AgdaAny
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)
            (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4)))
-- Type.BetaNBE.RenamingSubstitution.subNf-id
d_subNf'45'id_116 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'id_116 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
d_subNf'45'id_116 = T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-id'
d_subNf'45'id''_126 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'id''_126 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
d_subNf'45'id''_126 = T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-∋
d_subNf'45''8715'_142 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45''8715'_142 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8715''8902'__14
-> T__'8801'__12
d_subNf'45''8715'_142 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8715''8902'__14
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-nf
d_subNf'45'nf_160 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'nf_160 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'__12
d_subNf'45'nf_160 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866''8902'__20
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-comp
d_subNf'45'comp_182 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'comp_182 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'45'comp_182 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.extsNf
d_extsNf_198 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_extsNf_198 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
d_extsNf_198 ~T_Ctx'8902'_2
v0 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 T_Kind_476
v3 T_Kind_476
v4 T__'8715''8902'__14
v5 = T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
du_extsNf_198 T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 T_Kind_476
v3 T_Kind_476
v4 T__'8715''8902'__14
v5
du_extsNf_198 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_extsNf_198 :: T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
du_extsNf_198 T_Ctx'8902'_2
v0 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v1 T_Kind_476
v2 T_Kind_476
v3 T__'8715''8902'__14
v4
  = case T__'8715''8902'__14 -> T__'8715''8902'__14
forall a b. a -> b
coe T__'8715''8902'__14
v4 of
      T__'8715''8902'__14
MAlonzo.Code.Type.C_Z_16
        -> (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20
             ((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))
      MAlonzo.Code.Type.C_S_18 T__'8715''8902'__14
v8
        -> (T_Ctx'8902'_2
 -> T_Kind_476
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> AgdaAny
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 T_Ctx'8902'_2
v0 T_Kind_476
v3 T_Kind_476
v2 ((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8715''8902'__14 -> AgdaAny
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v1 T_Kind_476
v3 T__'8715''8902'__14
v8)
      T__'8715''8902'__14
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.RenamingSubstitution.subNf-cons
d_subNf'45'cons_218 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_subNf'45'cons_218 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
d_subNf'45'cons_218 ~T_Ctx'8902'_2
v0 ~T_Ctx'8902'_2
v1 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 ~T_Kind_476
v3 T__'8866'Nf'8902'__4
v4 T_Kind_476
v5 T__'8715''8902'__14
v6
  = (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
du_subNf'45'cons_218 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v2 T__'8866'Nf'8902'__4
v4 T_Kind_476
v5 T__'8715''8902'__14
v6
du_subNf'45'cons_218 ::
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T__'8715''8902'__14 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
du_subNf'45'cons_218 :: (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
du_subNf'45'cons_218 T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v0 T__'8866'Nf'8902'__4
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 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v1
      MAlonzo.Code.Type.C_S_18 T__'8715''8902'__14
v7 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4
v0 T_Kind_476
v2 T__'8715''8902'__14
v7
      T__'8715''8902'__14
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.RenamingSubstitution._[_]Nf
d__'91'_'93'Nf_236 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d__'91'_'93'Nf_236 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d__'91'_'93'Nf_236 T_Ctx'8902'_2
v0 T_Kind_476
v1 T_Kind_476
v2 T__'8866'Nf'8902'__4
v3 T__'8866'Nf'8902'__4
v4
  = (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
      T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_subNf_104
      ((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
v2)) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0)
      (((T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
 -> T__'8866'Nf'8902'__4
 -> T_Kind_476
 -> T__'8715''8902'__14
 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny -> AgdaAny
forall a b. a -> b
coe
         (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T_Kind_476
-> T__'8715''8902'__14
-> T__'8866'Nf'8902'__4
du_subNf'45'cons_218
         ((AgdaAny -> AgdaAny -> AgdaAny) -> AgdaAny
forall a b. a -> b
coe
            (\ AgdaAny
v5 AgdaAny
v6 ->
               (T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4)
-> AgdaAny -> AgdaAny
forall a b. a -> b
coe
                 T__'8866'Ne'8902'__6 -> T__'8866'Nf'8902'__4
MAlonzo.Code.Type.BetaNormal.C_ne_20
                 ((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 AgdaAny
v6)))
         (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v4))
      (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v3)
-- Type.BetaNBE.RenamingSubstitution.subNf-cong
d_subNf'45'cong_260 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  (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.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'cong_260 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8801'__12)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'45'cong_260 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8801'__12)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-cong'
d_subNf'45'cong''_280 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'cong''_280 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
d_subNf'45'cong''_280 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.renNf-subNf
d_renNf'45'subNf_300 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  (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.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_renNf'45'subNf_300 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_renNf'45'subNf_300 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-renNf
d_subNf'45'renNf_324 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  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__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'renNf_324 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'45'renNf_324 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.ren[]Nf
d_ren'91''93'Nf_350 ::
  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__'8715''8902'__14) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_ren'91''93'Nf_350 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_ren'91''93'Nf_350 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.sub[]Nf
d_sub'91''93'Nf_378 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'91''93'Nf_378 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_sub'91''93'Nf_378 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-lemma
d_subNf'45'lemma_404 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.T__'8866''8902'__20 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'lemma_404 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866''8902'__20
-> T__'8801'__12
d_subNf'45'lemma_404 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866''8902'__20
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-lemma'
d_subNf'45'lemma''_422 ::
  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.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'lemma''_422 :: T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8801'__12
d_subNf'45'lemma''_422 = T_Ctx'8902'_2
-> T_Kind_476 -> T_Kind_476 -> T__'8866''8902'__20 -> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.sub[]Nf'
d_sub'91''93'Nf''_446 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'91''93'Nf''_446 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_sub'91''93'Nf''_446 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.weakenNf-renNf
d_weakenNf'45'renNf_464 ::
  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.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_weakenNf'45'renNf_464 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_weakenNf'45'renNf_464 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.weakenNf-subNf
d_weakenNf'45'subNf_480 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_weakenNf'45'subNf_480 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_weakenNf'45'subNf_480 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.weakenNf[]
d_weakenNf'91''93'_494 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_weakenNf'91''93'_494 :: T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_weakenNf'91''93'_494 = T_Ctx'8902'_2
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.sub-nf-Π
d_sub'45'nf'45'Π_510 ::
  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.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'nf'45'Π_510 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_sub'45'nf'45'Π_510 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.sub-nf-μ
d_sub'45'nf'45'μ_528 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_sub'45'nf'45'μ_528 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_sub'45'nf'45'μ_528 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf-cons-[]Nf
d_subNf'45'cons'45''91''93'Nf_548 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  (MAlonzo.Code.Utils.T_Kind_476 ->
   MAlonzo.Code.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'45'cons'45''91''93'Nf_548 :: T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'45'cons'45''91''93'Nf_548 = T_Ctx'8902'_2
-> T_Kind_476
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf∅
d_subNf'8709'_566 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
d_subNf'8709'_566 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
d_subNf'8709'_566 T_Ctx'8902'_2
v0 T_Kind_476
v1 T__'8866'Nf'8902'__4
v2
  = case T_Ctx'8902'_2 -> T_Ctx'8902'_2
forall a b. a -> b
coe T_Ctx'8902'_2
v0 of
      T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4 -> T__'8866'Nf'8902'__4 -> T__'8866'Nf'8902'__4
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2
      MAlonzo.Code.Type.C__'44''8902'__6 T_Ctx'8902'_2
v3 T_Kind_476
v4
        -> (T_Ctx'8902'_2
 -> T_Ctx'8902'_2
 -> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
 -> T_Kind_476
 -> T__'8866'Nf'8902'__4
 -> T__'8866'Nf'8902'__4)
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> AgdaAny
-> T__'8866'Nf'8902'__4
forall a b. a -> b
coe
             T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T_Kind_476
-> T__'8866'Nf'8902'__4
-> T__'8866'Nf'8902'__4
d_subNf_104 (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
MAlonzo.Code.Type.C_'8709'_4) (T_Ctx'8902'_2 -> AgdaAny
forall a b. a -> b
coe T_Ctx'8902'_2
v0) AgdaAny
forall a. a
erased
             (T_Kind_476 -> AgdaAny
forall a b. a -> b
coe T_Kind_476
v1) (T__'8866'Nf'8902'__4 -> AgdaAny
forall a b. a -> b
coe T__'8866'Nf'8902'__4
v2)
      T_Ctx'8902'_2
_ -> T__'8866'Nf'8902'__4
forall a. a
MAlonzo.RTE.mazUnreachableError
-- Type.BetaNBE.RenamingSubstitution.subNf∅≡subNf
d_subNf'8709''8801'subNf_582 ::
  MAlonzo.Code.Type.T_Ctx'8902'_2 ->
  MAlonzo.Code.Utils.T_Kind_476 ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'8709''8801'subNf_582 :: T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
d_subNf'8709''8801'subNf_582 = T_Ctx'8902'_2
-> T_Kind_476 -> T__'8866'Nf'8902'__4 -> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf∅-renNf
d_subNf'8709''45'renNf_600 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.T__'8715''8902'__14) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'8709''45'renNf_600 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'8709''45'renNf_600 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8715''8902'__14)
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased
-- Type.BetaNBE.RenamingSubstitution.subNf∅-subNf
d_subNf'8709''45'subNf_616 ::
  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.Type.T__'8715''8902'__14 ->
   MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4) ->
  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
  MAlonzo.Code.Agda.Builtin.Equality.T__'8801'__12
d_subNf'8709''45'subNf_616 :: T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
d_subNf'8709''45'subNf_616 = T_Ctx'8902'_2
-> T_Ctx'8902'_2
-> T_Kind_476
-> (T_Kind_476 -> T__'8715''8902'__14 -> T__'8866'Nf'8902'__4)
-> T__'8866'Nf'8902'__4
-> T__'8801'__12
forall a. a
erased