content: {-# 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.Check where
  
  import MAlonzo.RTE (coe, erased, AgdaAny, addInt, subInt, mulInt,
                      quotInt, remInt, geqInt, ltInt, eqInt, add64, sub64, mul64, quot64,
                      rem64, lt64, eq64, word64FromNat, word64ToNat)
  import qualified MAlonzo.RTE
  import qualified Data.Text
  import qualified MAlonzo.Code.Agda.Builtin.Bool
  import qualified MAlonzo.Code.Agda.Builtin.Equality
  import qualified MAlonzo.Code.Agda.Builtin.List
  import qualified MAlonzo.Code.Agda.Builtin.Sigma
  import qualified MAlonzo.Code.Agda.Builtin.String
  import qualified MAlonzo.Code.Algorithmic
  import qualified MAlonzo.Code.Algorithmic.Signature
  import qualified MAlonzo.Code.Builtin.Constant.AtomicType
  import qualified MAlonzo.Code.Builtin.Constant.Type
  import qualified MAlonzo.Code.Data.Fin.Base
  import qualified MAlonzo.Code.Data.Irrelevant
  import qualified MAlonzo.Code.Data.Nat.Base
  import qualified MAlonzo.Code.Data.Nat.Properties
  import qualified MAlonzo.Code.Data.Vec.Base
  import qualified MAlonzo.Code.RawU
  import qualified MAlonzo.Code.Relation.Nullary.Decidable.Core
  import qualified MAlonzo.Code.Relation.Nullary.Reflects
  import qualified MAlonzo.Code.Scoped
  import qualified MAlonzo.Code.Type
  import qualified MAlonzo.Code.Type.BetaNBE
  import qualified MAlonzo.Code.Type.BetaNBE.RenamingSubstitution
  import qualified MAlonzo.Code.Type.BetaNormal
  import qualified MAlonzo.Code.Utils
  import qualified MAlonzo.Code.Utils.Decidable
  import qualified MAlonzo.Code.Utils.List
  
  -- Check.TypeError
  d_TypeError_12 = ()
  data T_TypeError_12
    = C_kindMismatch_18 MAlonzo.Code.Utils.T_Kind_652
                        MAlonzo.Code.Utils.T_Kind_652 |
      C_notFunKind_26 MAlonzo.Code.Utils.T_Kind_652 |
      C_notPat_32 MAlonzo.Code.Utils.T_Kind_652 | C_UnknownType_34 |
      C_notPi_44 MAlonzo.Code.Type.T_Ctx'8902'_2
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
      C_notMu_56 MAlonzo.Code.Type.T_Ctx'8902'_2
                 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
      C_notFunType_66 MAlonzo.Code.Type.T_Ctx'8902'_2
                      MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
      C_notSOP_76 MAlonzo.Code.Type.T_Ctx'8902'_2
                  MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
      C_IndexOutOfBounds_82 Integer Integer | C_TooManyConstrArgs_84 |
      C_TooFewConstrArgs_86 | C_TooFewCases_88 | C_TooManyCases_90 |
      C_typeMismatch_100 MAlonzo.Code.Type.T_Ctx'8902'_2
                         MAlonzo.Code.Utils.T_Kind_652
                         MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
                         MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 |
      C_builtinError_102 |
      C_Unimplemented_104 MAlonzo.Code.Agda.Builtin.String.T_String_6
  -- Check.len⋆
  d_len'8902'_106 :: MAlonzo.Code.Type.T_Ctx'8902'_2 -> Integer
  d_len'8902'_106 v0
    = case coe v0 of
        MAlonzo.Code.Type.C_'8709'_4 -> coe (0 :: Integer)
        MAlonzo.Code.Type.C__'44''8902'__6 v1 v2
          -> coe addInt (coe (1 :: Integer)) (coe d_len'8902'_106 (coe v1))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.inferTyVar
  d_inferTyVar_118 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Data.Fin.Base.T_Fin_10 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inferTyVar_118 v0 v1
    = case coe v0 of
        MAlonzo.Code.Type.C__'44''8902'__6 v2 v3
          -> case coe v1 of
               MAlonzo.Code.Data.Fin.Base.C_zero_12
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v3)
                      (coe MAlonzo.Code.Type.C_Z_16)
               MAlonzo.Code.Data.Fin.Base.C_suc_16 v5
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                         (coe d_inferTyVar_118 (coe v2) (coe v5)))
                      (coe
                         MAlonzo.Code.Type.C_S_18
                         (MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                            (coe d_inferTyVar_118 (coe v2) (coe v5))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decKind
  d_decKind_138 ::
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decKind_138 v0 v1
    = case coe v0 of
        MAlonzo.Code.Utils.C_'42'_654
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Utils.C__'8658'__658 v2 v3
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Utils.C_'9839'_656
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               MAlonzo.Code.Utils.C__'8658'__658 v2 v3
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Utils.C__'8658'__658 v2 v3
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Utils.C__'8658'__658 v4 v5
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong'8322'_70
                      (coe d_decKind_138 (coe v2) (coe v4))
                      (coe d_decKind_138 (coe v3) (coe v5))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isFunKind
  d_isFunKind_174 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isFunKind_174 ~v0 v1 = du_isFunKind_174 v1
  du_isFunKind_174 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isFunKind_174 v0
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v1 v2
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notFunKind_26 v1)
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notFunKind_26 v1)
               MAlonzo.Code.Utils.C__'8658'__658 v3 v4
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v3)
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v4) (coe v2)))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isPat
  d_isPat_196 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isPat_196 ~v0 v1 = du_isPat_196 v1
  du_isPat_196 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isPat_196 v0
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v1 v2
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
               MAlonzo.Code.Utils.C__'8658'__658 v3 v4
                 -> case coe v3 of
                      MAlonzo.Code.Utils.C_'42'_654
                        -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                      MAlonzo.Code.Utils.C_'9839'_656
                        -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                      MAlonzo.Code.Utils.C__'8658'__658 v5 v6
                        -> case coe v4 of
                             MAlonzo.Code.Utils.C_'42'_654
                               -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                             MAlonzo.Code.Utils.C_'9839'_656
                               -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                             MAlonzo.Code.Utils.C__'8658'__658 v7 v8
                               -> case coe v6 of
                                    MAlonzo.Code.Utils.C_'42'_654
                                      -> case coe v8 of
                                           MAlonzo.Code.Utils.C_'42'_654
                                             -> coe
                                                  MAlonzo.Code.Utils.du_eitherBind_42
                                                  (coe
                                                     MAlonzo.Code.Utils.du_withE_282
                                                     (\ v9 -> coe C_kindMismatch_18 (coe v5) (coe v7))
                                                     (coe
                                                        MAlonzo.Code.Utils.du_dec2Either_294
                                                        (coe d_decKind_138 (coe v5) (coe v7))))
                                                  (coe
                                                     (\ v9 ->
                                                        coe
                                                          MAlonzo.Code.Utils.C_inj'8322'_14
                                                          (coe
                                                             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                             (coe v5) (coe v2))))
                                           MAlonzo.Code.Utils.C_'9839'_656
                                             -> coe
                                                  MAlonzo.Code.Utils.C_inj'8321'_12
                                                  (coe C_notPat_32 v1)
                                           MAlonzo.Code.Utils.C__'8658'__658 v9 v10
                                             -> coe
                                                  MAlonzo.Code.Utils.C_inj'8321'_12
                                                  (coe C_notPat_32 v1)
                                           _ -> MAlonzo.RTE.mazUnreachableError
                                    MAlonzo.Code.Utils.C_'9839'_656
                                      -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                                    MAlonzo.Code.Utils.C__'8658'__658 v9 v10
                                      -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_notPat_32 v1)
                                    _ -> MAlonzo.RTE.mazUnreachableError
                             _ -> MAlonzo.RTE.mazUnreachableError
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isPi
  d_isPi_296 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isPi_296 v0 ~v1 v2 = du_isPi_296 v0 v2
  du_isPi_296 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isPi_296 v0 v1
    = case coe v1 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6) (coe v3)))
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notPi_44 v0
                         (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notPi_44 v0 (coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v6))
               MAlonzo.Code.Type.BetaNormal.C_con_22 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notPi_44 v0 (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v5))
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notPi_44 v0 (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7))
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notPi_44 v0 (coe MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isFunType
  d_isFunType_338 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isFunType_338 v0 ~v1 v2 = du_isFunType_338 v0 v2
  du_isFunType_338 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isFunType_338 v0 v1
    = case coe v1 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notFunType_66 v0 (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6) (coe v3)))
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notFunType_66 v0 (coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v6))
               MAlonzo.Code.Type.BetaNormal.C_con_22 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notFunType_66 v0 (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v5))
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notFunType_66 v0
                         (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7))
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notFunType_66 v0
                         (coe MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isMu
  d_isMu_392 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isMu_392 v0 ~v1 v2 = du_isMu_392 v0 v2
  du_isMu_392 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isMu_392 v0 v1
    = case coe v1 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notMu_56 v0 (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notMu_56 v0
                         (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notMu_56 v0 (coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v6))
               MAlonzo.Code.Type.BetaNormal.C_con_22 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notMu_56 v0 (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v5))
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6)
                            (coe
                               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v7) (coe v3))))
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notMu_56 v0 (coe MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isSOPType
  d_isSOPType_436 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isSOPType_436 v0 v1
    = case coe v1 of
        MAlonzo.Code.Type.BetaNormal.C_Π_14 v3 v4
          -> coe
               MAlonzo.Code.Utils.C_inj'8321'_12
               (coe
                  C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v3 v4))
        MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v3 v4
          -> coe
               MAlonzo.Code.Utils.C_inj'8321'_12
               (coe
                  C_notSOP_76 v0
                  (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v3 v4))
        MAlonzo.Code.Type.BetaNormal.C_ne_20 v4
          -> coe
               MAlonzo.Code.Utils.C_inj'8321'_12
               (coe C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v4))
        MAlonzo.Code.Type.BetaNormal.C_con_22 v3
          -> coe
               MAlonzo.Code.Utils.C_inj'8321'_12
               (coe C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v3))
        MAlonzo.Code.Type.BetaNormal.C_μ_24 v3 v4 v5
          -> coe
               MAlonzo.Code.Utils.C_inj'8321'_12
               (coe
                  C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v3 v4 v5))
        MAlonzo.Code.Type.BetaNormal.C_SOP_28 v3 v4
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v3) (coe v4))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.isSOP
  d_isSOP_476 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_isSOP_476 v0 ~v1 v2 = du_isSOP_476 v0 v2
  du_isSOP_476 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_isSOP_476 v0 v1
    = case coe v1 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notSOP_76 v0
                         (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6))
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_ne_20 v6))
               MAlonzo.Code.Type.BetaNormal.C_con_22 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v5))
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12
                      (coe
                         C_notSOP_76 v0 (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7))
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                         (coe
                            MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6) (coe v3)))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.chkIdx
  d_chkIdx_514 ::
    Integer ->
    Integer ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Data.Fin.Base.T_Fin_10
  d_chkIdx_514 v0 v1
    = let v2
            = coe
                MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                (\ v2 ->
                   coe
                     MAlonzo.Code.Data.Nat.Properties.du_'8804''7495''8658''8804'_2746
                     (coe addInt (coe (1 :: Integer)) (coe v0)))
                (coe
                   MAlonzo.Code.Data.Nat.Properties.du_'8804''8658''8804''7495'_2758)
                (coe
                   MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                   (coe
                      MAlonzo.Code.Data.Nat.Base.d__'8804''7495'__14
                      (coe addInt (coe (1 :: Integer)) (coe v0)) (coe v1))) in
      coe
        (case coe v2 of
           MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v3 v4
             -> if coe v3
                  then coe
                         seq (coe v4)
                         (coe
                            MAlonzo.Code.Utils.C_inj'8322'_14
                            (coe MAlonzo.Code.Data.Fin.Base.du_fromℕ'60'_52 (coe v0)))
                  else coe
                         seq (coe v4)
                         (coe
                            MAlonzo.Code.Utils.C_inj'8321'_12
                            (coe C_IndexOutOfBounds_82 v0 v1))
           _ -> MAlonzo.RTE.mazUnreachableError)
  -- Check.inferTyCon
  d_inferTyCon_542 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inferTyCon_542 ~v0 v1 v2 = du_inferTyCon_542 v1 v2
  du_inferTyCon_542 ::
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_inferTyCon_542 v0 v1
    = coe
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v0)
        (coe
           MAlonzo.Code.Type.BetaNormal.C_ne_20
           (coe MAlonzo.Code.Type.BetaNormal.C_'94'_12 v1))
  -- Check.checkKind
  d_checkKind_554 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
  d_checkKind_554 v0 v1 v2
    = coe
        MAlonzo.Code.Utils.du_eitherBind_42
        (coe d_inferKind_562 (coe v0) (coe v1))
        (coe (\ v3 -> coe du_checkKind'45'aux_606 (coe v3) (coe v2)))
  -- Check.inferKind
  d_inferKind_562 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inferKind_562 v0 v1
    = case coe v1 of
        MAlonzo.Code.Scoped.C_'96'_18 v2
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe
                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                  (coe
                     MAlonzo.Code.Agda.Builtin.Sigma.d_fst_28
                     (coe d_inferTyVar_118 (coe v0) (coe v2)))
                  (coe
                     MAlonzo.Code.Type.BetaNormal.C_ne_20
                     (coe
                        MAlonzo.Code.Type.BetaNormal.C_'96'_8
                        (MAlonzo.Code.Agda.Builtin.Sigma.d_snd_30
                           (coe d_inferTyVar_118 (coe v0) (coe v2))))))
        MAlonzo.Code.Scoped.C__'8658'__20 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v2)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe
                          d_checkKind_554 (coe v0) (coe v3)
                          (coe MAlonzo.Code.Utils.C_'42'_654))
                       (coe
                          (\ v5 ->
                             coe
                               MAlonzo.Code.Utils.C_inj'8322'_14
                               (coe
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                  (coe MAlonzo.Code.Utils.C_'42'_654)
                                  (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v4 v5))))))
        MAlonzo.Code.Scoped.C_Π_22 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554
                  (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v2)) (coe v3)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.C_inj'8322'_14
                       (coe
                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                          (coe MAlonzo.Code.Utils.C_'42'_654)
                          (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v2 v4))))
        MAlonzo.Code.Scoped.C_ƛ_24 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_inferKind_562
                  (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v2))
                  (coe v3))
               (coe
                  (\ v4 ->
                     case coe v4 of
                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
                         -> coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 (coe MAlonzo.Code.Utils.C__'8658'__658 (coe v2) (coe v5))
                                 (coe MAlonzo.Code.Type.BetaNormal.C_ƛ_18 v6))
                       _ -> MAlonzo.RTE.mazUnreachableError))
        MAlonzo.Code.Scoped.C__'183'__26 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferKind_562 (coe v0) (coe v2))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42 (coe du_isFunKind_174 (coe v4))
                       (coe du_'46'extendedlambda4_710 (coe v0) (coe v3))))
        MAlonzo.Code.Scoped.C_con_30 v2 v3
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe du_addCon_658 (coe du_inferTyCon_542 (coe v2) (coe v3)))
        MAlonzo.Code.Scoped.C_μ_32 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferKind_562 (coe v0) (coe v2))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42 (coe du_isPat_196 (coe v4))
                       (coe du_'46'extendedlambda4_732 (coe v0) (coe v3))))
        MAlonzo.Code.Scoped.C_SOP_34 v2
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferKind'45'VecList_586 (coe v0) (coe v2))
               (coe
                  (\ v3 ->
                     coe
                       MAlonzo.Code.Utils.C_inj'8322'_14
                       (coe
                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                          (coe MAlonzo.Code.Utils.C_'42'_654)
                          (coe
                             MAlonzo.Code.Type.BetaNormal.C_SOP_28
                             (coe MAlonzo.Code.Utils.du_length_394 (coe v2)) v3))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.inferKind-List
  d_inferKind'45'List_568 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4]
  d_inferKind'45'List_568 v0 v1
    = case coe v1 of
        MAlonzo.Code.Utils.C_'91''93'_388
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe MAlonzo.Code.Agda.Builtin.List.C_'91''93'_16)
        MAlonzo.Code.Utils.C__'8759'__390 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v2)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe d_inferKind'45'List_568 (coe v0) (coe v3))
                       (coe
                          (\ v5 ->
                             coe
                               MAlonzo.Code.Utils.C_inj'8322'_14
                               (coe
                                  MAlonzo.Code.Agda.Builtin.List.C__'8759'__22 (coe v4) (coe v5))))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.inferKind-VecList
  d_inferKind'45'VecList_586 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_List_384
      (MAlonzo.Code.Utils.T_List_384
         MAlonzo.Code.Scoped.T_ScopedTy_14) ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Data.Vec.Base.T_Vec_28
  d_inferKind'45'VecList_586 v0 v1
    = case coe v1 of
        MAlonzo.Code.Utils.C_'91''93'_388
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe MAlonzo.Code.Data.Vec.Base.C_'91''93'_32)
        MAlonzo.Code.Utils.C__'8759'__390 v2 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferKind'45'List_568 (coe v0) (coe v2))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe d_inferKind'45'VecList_586 (coe v0) (coe v3))
                       (coe
                          (\ v5 ->
                             coe
                               MAlonzo.Code.Utils.C_inj'8322'_14
                               (coe MAlonzo.Code.Data.Vec.Base.C__'8759'__38 v4 v5)))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.checkKind-aux
  d_checkKind'45'aux_606 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
  d_checkKind'45'aux_606 ~v0 v1 v2 = du_checkKind'45'aux_606 v1 v2
  du_checkKind'45'aux_606 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4
  du_checkKind'45'aux_606 v0 v1
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v2 v3
          -> case coe v2 of
               MAlonzo.Code.Utils.C_'42'_654
                 -> case coe v1 of
                      MAlonzo.Code.Utils.C_'42'_654
                        -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe v3)
                      MAlonzo.Code.Utils.C_'9839'_656
                        -> let v4
                                 = coe
                                     MAlonzo.Code.Utils.C_inj'8321'_12
                                     (coe C_kindMismatch_18 v1 v2) in
                           coe
                             (case coe v3 of
                                MAlonzo.Code.Type.BetaNormal.C_con_22 v6
                                  -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe v6)
                                _ -> coe v4)
                      MAlonzo.Code.Utils.C__'8658'__658 v4 v5
                        -> coe
                             MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_kindMismatch_18 v2 v1)
                      _ -> MAlonzo.RTE.mazUnreachableError
               MAlonzo.Code.Utils.C_'9839'_656
                 -> case coe v1 of
                      MAlonzo.Code.Utils.C_'42'_654
                        -> coe
                             MAlonzo.Code.Utils.C_inj'8322'_14
                             (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v3)
                      MAlonzo.Code.Utils.C_'9839'_656
                        -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe v3)
                      MAlonzo.Code.Utils.C__'8658'__658 v4 v5
                        -> coe
                             MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_kindMismatch_18 v2 v1)
                      _ -> MAlonzo.RTE.mazUnreachableError
               MAlonzo.Code.Utils.C__'8658'__658 v4 v5
                 -> case coe v1 of
                      MAlonzo.Code.Utils.C_'42'_654
                        -> coe
                             MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_kindMismatch_18 v2 v1)
                      MAlonzo.Code.Utils.C_'9839'_656
                        -> coe
                             MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_kindMismatch_18 v2 v1)
                      MAlonzo.Code.Utils.C__'8658'__658 v6 v7
                        -> coe
                             MAlonzo.Code.Utils.du_eitherBind_42
                             (coe
                                MAlonzo.Code.Utils.du_withE_282
                                (\ v8 -> coe C_kindMismatch_18 (coe v2) (coe v1))
                                (coe
                                   MAlonzo.Code.Utils.du_dec2Either_294
                                   (coe d_decKind_138 (coe v2) (coe v1))))
                             (coe (\ v8 -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe v3)))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.addCon
  d_addCon_658 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_addCon_658 ~v0 v1 = du_addCon_658 v1
  du_addCon_658 ::
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_addCon_658 v0
    = case coe v0 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v1 v2
          -> case coe v1 of
               MAlonzo.Code.Utils.C_'9839'_656
                 -> coe
                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                      (coe MAlonzo.Code.Utils.C_'42'_654)
                      (coe MAlonzo.Code.Type.BetaNormal.C_con_22 v2)
               _ -> coe v0
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda4
  d_'46'extendedlambda4_710 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda4_710 v0 ~v1 v2 ~v3 v4
    = du_'46'extendedlambda4_710 v0 v2 v4
  du_'46'extendedlambda4_710 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda4_710 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
          -> case coe v4 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe d_checkKind_554 (coe v0) (coe v1) (coe v3))
                      (coe
                         (\ v7 ->
                            coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 du_addCon_658
                                 (coe
                                    MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                                    (coe
                                       MAlonzo.Code.Type.BetaNBE.d_nf_258 (coe v0) (coe v5)
                                       (coe
                                          MAlonzo.Code.Type.C__'183'__30 v3
                                          (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                             (coe v0)
                                             (coe MAlonzo.Code.Utils.C__'8658'__658 (coe v3) (coe v5))
                                             (coe v6))
                                          (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                             (coe v0) (coe v3) (coe v7))))))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda4
  d_'46'extendedlambda4_732 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda4_732 v0 ~v1 v2 ~v3 v4
    = du_'46'extendedlambda4_732 v0 v2 v4
  du_'46'extendedlambda4_732 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda4_732 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v3 v4
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_checkKind_554 (coe v0) (coe v1) (coe v3))
               (coe
                  (\ v5 ->
                     coe
                       MAlonzo.Code.Utils.C_inj'8322'_14
                       (coe
                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                          (coe MAlonzo.Code.Utils.C_'42'_654)
                          (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v3 v4 v5))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.len
  d_len_776 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 -> MAlonzo.Code.Scoped.T_Weirdℕ_42
  d_len_776 v0 v1
    = case coe v1 of
        MAlonzo.Code.Algorithmic.C_'8709'_4
          -> coe MAlonzo.Code.Scoped.C_Z_44
        MAlonzo.Code.Algorithmic.C__'44''8902'__8 v3
          -> case coe v0 of
               MAlonzo.Code.Type.C__'44''8902'__6 v5 v6
                 -> coe MAlonzo.Code.Scoped.C_T_52 (d_len_776 (coe v5) (coe v3))
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Algorithmic.C__'44'__12 v3 v4
          -> coe MAlonzo.Code.Scoped.C_S_48 (d_len_776 (coe v0) (coe v3))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.inferVarType
  d_inferVarType_792 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_WeirdFin_56 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inferVarType_792 v0 v1 v2
    = case coe v1 of
        MAlonzo.Code.Algorithmic.C__'44''8902'__8 v4
          -> case coe v0 of
               MAlonzo.Code.Type.C__'44''8902'__6 v6 v7
                 -> case coe v2 of
                      MAlonzo.Code.Scoped.C_T_74 v10
                        -> coe
                             MAlonzo.Code.Utils.du_eitherBind_42
                             (coe d_inferVarType_792 (coe v6) (coe v4) (coe v10))
                             (coe
                                (\ v11 ->
                                   case coe v11 of
                                     MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v12 v13
                                       -> coe
                                            MAlonzo.Code.Utils.C_inj'8322'_14
                                            (coe
                                               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                               (coe
                                                  MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 v6
                                                  (coe MAlonzo.Code.Utils.C_'42'_654) v7 v12)
                                               (coe MAlonzo.Code.Algorithmic.C_T_38 v12 v13))
                                     _ -> MAlonzo.RTE.mazUnreachableError))
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Algorithmic.C__'44'__12 v4 v5
          -> case coe v2 of
               MAlonzo.Code.Scoped.C_Z_62
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                         (coe MAlonzo.Code.Algorithmic.C_Z_22))
               MAlonzo.Code.Scoped.C_S_68 v8
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe d_inferVarType_792 (coe v0) (coe v4) (coe v8))
                      (coe
                         (\ v9 ->
                            case coe v9 of
                              MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v10 v11
                                -> coe
                                     MAlonzo.Code.Utils.C_inj'8322'_14
                                     (coe
                                        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v10)
                                        (coe MAlonzo.Code.Algorithmic.C_S_30 v11))
                              _ -> MAlonzo.RTE.mazUnreachableError))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decTyVar
  d_decTyVar_830 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Type.T__'8715''8902'__14 ->
    MAlonzo.Code.Type.T__'8715''8902'__14 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decTyVar_830 v0 ~v1 v2 v3 = du_decTyVar_830 v0 v2 v3
  du_decTyVar_830 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Type.T__'8715''8902'__14 ->
    MAlonzo.Code.Type.T__'8715''8902'__14 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_decTyVar_830 v0 v1 v2
    = case coe v1 of
        MAlonzo.Code.Type.C_Z_16
          -> case coe v2 of
               MAlonzo.Code.Type.C_Z_16
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               MAlonzo.Code.Type.C_S_18 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.C_S_18 v6
          -> case coe v0 of
               MAlonzo.Code.Type.C__'44''8902'__6 v7 v8
                 -> case coe v2 of
                      MAlonzo.Code.Type.C_Z_16
                        -> coe
                             MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                             (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                             (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                      MAlonzo.Code.Type.C_S_18 v12
                        -> let v13 = coe du_decTyVar_830 (coe v7) (coe v6) (coe v12) in
                           coe
                             (case coe v13 of
                                MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v14 v15
                                  -> if coe v14
                                       then coe
                                              seq (coe v15)
                                              (coe
                                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                 (coe v14)
                                                 (coe
                                                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                    erased))
                                       else coe
                                              seq (coe v15)
                                              (coe
                                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                 (coe v14)
                                                 (coe
                                                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                                _ -> MAlonzo.RTE.mazUnreachableError)
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decNfTy
  d_decNfTy_864 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decNfTy_864 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Type.BetaNormal.C_Π_14 v5 v6
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v8 v9
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dhcong_120 (coe v9)
                      (coe d_decKind_138 (coe v5) (coe v8))
                      (coe
                         d_decNfTy_864
                         (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v5))
                         (coe MAlonzo.Code.Utils.C_'42'_654) (coe v6))
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_con_22 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v8 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v6
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v8 v9
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong'8322'_70
                      (coe
                         d_decNfTy_864 (coe v0) (coe MAlonzo.Code.Utils.C_'42'_654) (coe v5)
                         (coe v8))
                      (coe
                         d_decNfTy_864 (coe v0) (coe MAlonzo.Code.Utils.C_'42'_654) (coe v6)
                         (coe v9))
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_con_22 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v8 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_ƛ_18 v7
          -> case coe v1 of
               MAlonzo.Code.Utils.C__'8658'__658 v8 v9
                 -> case coe v3 of
                      MAlonzo.Code.Type.BetaNormal.C_ƛ_18 v13
                        -> coe
                             MAlonzo.Code.Utils.Decidable.du_dcong_40
                             (d_decNfTy_864
                                (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v8)) (coe v9)
                                (coe v7) (coe v13))
                      MAlonzo.Code.Type.BetaNormal.C_ne_20 v12
                        -> coe
                             MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                             (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                             (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
                      _ -> MAlonzo.RTE.mazUnreachableError
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_ne_20 v6
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ƛ_18 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v9
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong_40
                      (coe du_decNeTy_874 (coe v0) (coe v6) (coe v9))
               MAlonzo.Code.Type.BetaNormal.C_con_22 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v8 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_con_22 v5
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v7 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v7 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_con_22 v7
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong_40
                      (d_decNfTy_864
                         (coe v0) (coe MAlonzo.Code.Utils.C_'9839'_656) (coe v5) (coe v7))
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v7 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v7 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_con_22 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v9 v10 v11
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dhcong'8322'_180 (coe v10)
                      (coe v11) (coe d_decKind_138 (coe v5) (coe v9))
                      (coe
                         d_decNfTy_864 (coe v0)
                         (coe
                            MAlonzo.Code.Utils.C__'8658'__658
                            (coe
                               MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                               (coe MAlonzo.Code.Utils.C_'42'_654))
                            (coe
                               MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                               (coe MAlonzo.Code.Utils.C_'42'_654)))
                         (coe v6))
                      (coe d_decNfTy_864 (coe v0) (coe v5) (coe v7))
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6
          -> case coe v3 of
               MAlonzo.Code.Type.BetaNormal.C_Π_14 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v8 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_ne_20 v9
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_con_22 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_μ_24 v8 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_SOP_28 v8 v9
                 -> let v10
                          = coe
                              MAlonzo.Code.Relation.Nullary.Decidable.Core.du_map'8242'_168
                              erased
                              (\ v10 ->
                                 coe
                                   MAlonzo.Code.Data.Nat.Properties.du_'8801''8658''8801''7495'_2678
                                   (coe v5))
                              (coe
                                 MAlonzo.Code.Relation.Nullary.Decidable.Core.d_T'63'_66
                                 (coe eqInt (coe v5) (coe v8))) in
                    coe
                      (case coe v10 of
                         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v11 v12
                           -> if coe v11
                                then coe
                                       seq (coe v12)
                                       (let v13
                                              = coe
                                                  du_decNfTy'45'VecList_914 (coe v0)
                                                  (coe MAlonzo.Code.Utils.C_'42'_654) (coe v6)
                                                  (coe v9) in
                                        coe
                                          (case coe v13 of
                                             MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 v14 v15
                                               -> if coe v14
                                                    then coe
                                                           seq (coe v15)
                                                           (coe
                                                              MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                              (coe v14)
                                                              (coe
                                                                 MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                                 erased))
                                                    else coe
                                                           seq (coe v15)
                                                           (coe
                                                              MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                              (coe v14)
                                                              (coe
                                                                 MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                                             _ -> MAlonzo.RTE.mazUnreachableError))
                                else coe
                                       seq (coe v12)
                                       (coe
                                          MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                          (coe v11)
                                          (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                         _ -> MAlonzo.RTE.mazUnreachableError)
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decNeTy
  d_decNeTy_874 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decNeTy_874 v0 ~v1 v2 v3 = du_decNeTy_874 v0 v2 v3
  du_decNeTy_874 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Ne'8902'__6 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_decNeTy_874 v0 v1 v2
    = case coe v1 of
        MAlonzo.Code.Type.BetaNormal.C_'96'_8 v5
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_'96'_8 v8
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong_40
                      (coe du_decTyVar_830 (coe v0) (coe v5) (coe v8))
               MAlonzo.Code.Type.BetaNormal.C__'183'__10 v7 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_'94'_12 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C__'183'__10 v4 v6 v7
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_'96'_8 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'183'__10 v9 v11 v12
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dhcong'8322'_180 (coe v11)
                      (coe v12) (coe d_decKind_138 (coe v4) (coe v9))
                      (coe du_decNeTy_874 (coe v0) (coe v6))
                      (coe d_decNfTy_864 (coe v0) (coe v4) (coe v7))
               MAlonzo.Code.Type.BetaNormal.C_'94'_12 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Type.BetaNormal.C_'94'_12 v5
          -> case coe v2 of
               MAlonzo.Code.Type.BetaNormal.C_'96'_8 v8
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C__'183'__10 v7 v9 v10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Type.BetaNormal.C_'94'_12 v8
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong_40
                      (coe du_decTyCon_932 (coe v5) (coe v8))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decNfTy-List
  d_decNfTy'45'List_884 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
    [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decNfTy'45'List_884 v0 v1 v2 v3
    = case coe v2 of
        []
          -> case coe v3 of
               []
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               (:) v4 v5
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        (:) v4 v5
          -> case coe v3 of
               []
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               (:) v6 v7
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong'8322'_70
                      (coe d_decNfTy_864 (coe v0) (coe v1) (coe v4) (coe v6))
                      (coe d_decNfTy'45'List_884 (coe v0) (coe v1) (coe v5) (coe v7))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decNfTy-VecList
  d_decNfTy'45'VecList_914 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    Integer ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decNfTy'45'VecList_914 v0 ~v1 v2 v3 v4
    = du_decNfTy'45'VecList_914 v0 v2 v3 v4
  du_decNfTy'45'VecList_914 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_decNfTy'45'VecList_914 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
          -> coe
               seq (coe v3)
               (coe
                  MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                  (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                  (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased))
        MAlonzo.Code.Data.Vec.Base.C__'8759'__38 v5 v6
          -> case coe v3 of
               MAlonzo.Code.Data.Vec.Base.C__'8759'__38 v8 v9
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong'8322'_70
                      (coe d_decNfTy'45'List_884 (coe v0) (coe v1) (coe v5) (coe v8))
                      (coe du_decNfTy'45'VecList_914 (coe v0) (coe v1) (coe v6) (coe v9))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.decTyCon
  d_decTyCon_932 ::
    MAlonzo.Code.Utils.T_Kind_652 ->
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  d_decTyCon_932 ~v0 v1 v2 = du_decTyCon_932 v1 v2
  du_decTyCon_932 ::
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Builtin.Constant.Type.T_TyCon_6 ->
    MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
  du_decTyCon_932 v0 v1
    = case coe v0 of
        MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 v2
          -> case coe v1 of
               MAlonzo.Code.Builtin.Constant.Type.C_atomic_8 v3
                 -> coe
                      MAlonzo.Code.Utils.Decidable.du_dcong_40
                      (MAlonzo.Code.Builtin.Constant.AtomicType.d_decAtomicTyCon_26
                         (coe v2) (coe v3))
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Builtin.Constant.Type.C_list_10
          -> case coe v1 of
               MAlonzo.Code.Builtin.Constant.Type.C_list_10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               MAlonzo.Code.Builtin.Constant.Type.C_array_12
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Builtin.Constant.Type.C_array_12
          -> case coe v1 of
               MAlonzo.Code.Builtin.Constant.Type.C_list_10
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_false_8)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26)
               MAlonzo.Code.Builtin.Constant.Type.C_array_12
                 -> coe
                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                      (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                      (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Builtin.Constant.Type.C_pair_14
          -> coe
               seq (coe v1)
               (coe
                  MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                  (coe MAlonzo.Code.Agda.Builtin.Bool.C_true_10)
                  (coe MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 erased))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.checkType
  d_checkType_1148 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Algorithmic.T__'8866'__178
  d_checkType_1148 v0 v1 v2 v3
    = coe
        MAlonzo.Code.Utils.du_eitherBind_42
        (coe d_inferType_1156 (coe v0) (coe v1) (coe v2))
        (coe
           (\ v4 ->
              case coe v4 of
                MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
                  -> coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe
                          MAlonzo.Code.Utils.du_withE_282
                          (\ v7 ->
                             coe
                               C_typeMismatch_100 (coe v0) (coe MAlonzo.Code.Utils.C_'42'_654)
                               (coe v3) (coe v5))
                          (coe
                             MAlonzo.Code.Utils.du_dec2Either_294
                             (coe
                                d_decNfTy_864 (coe v0) (coe MAlonzo.Code.Utils.C_'42'_654) (coe v3)
                                (coe v5))))
                       (coe (\ v7 -> coe MAlonzo.Code.Utils.C_inj'8322'_14 (coe v6)))
                _ -> MAlonzo.RTE.mazUnreachableError))
  -- Check.inferType
  d_inferType_1156 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_inferType_1156 v0 v1 v2
    = case coe v2 of
        MAlonzo.Code.Scoped.C_'96'_528 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferVarType_792 (coe v0) (coe v1) (coe v3))
               (coe
                  (\ v4 ->
                     case coe v4 of
                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
                         -> coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v5)
                                 (coe MAlonzo.Code.Algorithmic.C_'96'_184 v6))
                       _ -> MAlonzo.RTE.mazUnreachableError))
        MAlonzo.Code.Scoped.C_Λ_530 v3 v4
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_inferType_1156
                  (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v3))
                  (coe MAlonzo.Code.Algorithmic.C__'44''8902'__8 v1) (coe v4))
               (coe
                  (\ v5 ->
                     case coe v5 of
                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v6 v7
                         -> coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                 (coe MAlonzo.Code.Type.BetaNormal.C_Π_14 v3 v6)
                                 (coe MAlonzo.Code.Algorithmic.C_Λ_202 v7))
                       _ -> MAlonzo.RTE.mazUnreachableError))
        MAlonzo.Code.Scoped.C__'183''8902'__532 v3 v4
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferType_1156 (coe v0) (coe v1) (coe v3))
               (coe
                  (\ v5 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe du_isPi_296 (coe v0) (coe v5))
                       (coe
                          (\ v6 ->
                             case coe v6 of
                               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v7 v8
                                 -> case coe v8 of
                                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v9 v10
                                        -> coe
                                             MAlonzo.Code.Utils.du_eitherBind_42
                                             (coe d_checkKind_554 (coe v0) (coe v4) (coe v7))
                                             (coe
                                                (\ v11 ->
                                                   coe
                                                     MAlonzo.Code.Utils.C_inj'8322'_14
                                                     (coe
                                                        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                        (coe
                                                           MAlonzo.Code.Type.BetaNBE.RenamingSubstitution.d__'91'_'93'Nf_236
                                                           (coe v0)
                                                           (coe MAlonzo.Code.Utils.C_'42'_654)
                                                           (coe v7) (coe v9) (coe v11))
                                                        (coe
                                                           MAlonzo.Code.Algorithmic.C__'183''8902'_'47'__212
                                                           v7 v9 v10 v11))))
                                      _ -> MAlonzo.RTE.mazUnreachableError
                               _ -> MAlonzo.RTE.mazUnreachableError))))
        MAlonzo.Code.Scoped.C_ƛ_534 v3 v4
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v3)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v5 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe
                          d_inferType_1156 (coe v0)
                          (coe MAlonzo.Code.Algorithmic.C__'44'__12 v1 v5) (coe v4))
                       (coe
                          (\ v6 ->
                             case coe v6 of
                               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v7 v8
                                 -> coe
                                      MAlonzo.Code.Utils.C_inj'8322'_14
                                      (coe
                                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                         (coe MAlonzo.Code.Type.BetaNormal.C__'8658'__16 v5 v7)
                                         (coe MAlonzo.Code.Algorithmic.C_ƛ_190 v8))
                               _ -> MAlonzo.RTE.mazUnreachableError))))
        MAlonzo.Code.Scoped.C__'183'__536 v3 v4
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferType_1156 (coe v0) (coe v1) (coe v3))
               (coe
                  (\ v5 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe du_isFunType_338 (coe v0) (coe v5))
                       (coe du_'46'extendedlambda24_1314 (coe v0) (coe v1) (coe v4))))
        MAlonzo.Code.Scoped.C_con_538 v3
          -> case coe v3 of
               MAlonzo.Code.RawU.C_tmCon_206 v4 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe
                         MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                         (coe
                            MAlonzo.Code.Type.BetaNormal.C_con_22
                            (MAlonzo.Code.Type.BetaNBE.RenamingSubstitution.d_subNf'8709'_566
                               (coe v0) (coe MAlonzo.Code.Utils.C_'9839'_656)
                               (coe MAlonzo.Code.Algorithmic.d_sty2ty_84 (coe v4))))
                         (coe
                            MAlonzo.Code.Algorithmic.C_con_258
                            (MAlonzo.Code.Algorithmic.d_sty2ty_84 (coe v4)) v5))
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Scoped.C_error_540 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v3)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.C_inj'8322'_14
                       (coe
                          MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v4)
                          (coe MAlonzo.Code.Algorithmic.C_error_268))))
        MAlonzo.Code.Scoped.C_builtin_544 v3
          -> coe
               MAlonzo.Code.Utils.C_inj'8322'_14
               (coe
                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                  (coe
                     MAlonzo.Code.Algorithmic.Signature.d_btype_30 (coe v0) (coe v3))
                  (coe MAlonzo.Code.Algorithmic.C_builtin_'47'__264 v3))
        MAlonzo.Code.Scoped.C_wrap_546 v3 v4 v5
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferKind_562 (coe v0) (coe v3))
               (coe
                  (\ v6 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42 (coe du_isPat_196 (coe v6))
                       (coe
                          du_'46'extendedlambda24_1352 (coe v0) (coe v1) (coe v4) (coe v5))))
        MAlonzo.Code.Scoped.C_unwrap_548 v3
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_inferType_1156 (coe v0) (coe v1) (coe v3))
               (coe
                  (\ v4 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe du_isMu_392 (coe v0) (coe v4))
                       (coe
                          (\ v5 ->
                             case coe v5 of
                               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v6 v7
                                 -> case coe v7 of
                                      MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v8 v9
                                        -> case coe v9 of
                                             MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v10 v11
                                               -> coe
                                                    MAlonzo.Code.Utils.C_inj'8322'_14
                                                    (coe
                                                       MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                                       (coe
                                                          MAlonzo.Code.Type.BetaNBE.d_nf_258 (coe v0)
                                                          (coe MAlonzo.Code.Utils.C_'42'_654)
                                                          (coe
                                                             MAlonzo.Code.Type.C__'183'__30 v6
                                                             (coe
                                                                MAlonzo.Code.Type.C__'183'__30
                                                                (coe
                                                                   MAlonzo.Code.Utils.C__'8658'__658
                                                                   (coe v6)
                                                                   (coe
                                                                      MAlonzo.Code.Utils.C_'42'_654))
                                                                (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                                                   (coe v0)
                                                                   (coe
                                                                      MAlonzo.Code.Utils.C__'8658'__658
                                                                      (coe
                                                                         MAlonzo.Code.Utils.C__'8658'__658
                                                                         (coe v6)
                                                                         (coe
                                                                            MAlonzo.Code.Utils.C_'42'_654))
                                                                      (coe
                                                                         MAlonzo.Code.Utils.C__'8658'__658
                                                                         (coe v6)
                                                                         (coe
                                                                            MAlonzo.Code.Utils.C_'42'_654)))
                                                                   (coe v8))
                                                                (coe
                                                                   MAlonzo.Code.Type.C_ƛ_28
                                                                   (coe
                                                                      MAlonzo.Code.Type.C_μ_32 v6
                                                                      (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                                                         (coe
                                                                            MAlonzo.Code.Type.C__'44''8902'__6
                                                                            (coe v0) (coe v6))
                                                                         (coe
                                                                            MAlonzo.Code.Utils.C__'8658'__658
                                                                            (coe
                                                                               MAlonzo.Code.Utils.C__'8658'__658
                                                                               (coe v6)
                                                                               (coe
                                                                                  MAlonzo.Code.Utils.C_'42'_654))
                                                                            (coe
                                                                               MAlonzo.Code.Utils.C__'8658'__658
                                                                               (coe v6)
                                                                               (coe
                                                                                  MAlonzo.Code.Utils.C_'42'_654)))
                                                                         (coe
                                                                            MAlonzo.Code.Type.BetaNormal.d_weakenNf_122
                                                                            v0
                                                                            (coe
                                                                               MAlonzo.Code.Utils.C__'8658'__658
                                                                               (coe
                                                                                  MAlonzo.Code.Utils.C__'8658'__658
                                                                                  (coe v6)
                                                                                  (coe
                                                                                     MAlonzo.Code.Utils.C_'42'_654))
                                                                               (coe
                                                                                  MAlonzo.Code.Utils.C__'8658'__658
                                                                                  (coe v6)
                                                                                  (coe
                                                                                     MAlonzo.Code.Utils.C_'42'_654)))
                                                                            v6 v8))
                                                                      (coe
                                                                         MAlonzo.Code.Type.C_'96'_22
                                                                         (coe
                                                                            MAlonzo.Code.Type.C_Z_16)))))
                                                             (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                                                (coe v0) (coe v6) (coe v10))))
                                                       (coe
                                                          MAlonzo.Code.Algorithmic.C_unwrap_230 v6 v8
                                                          v10 v11))
                                             _ -> MAlonzo.RTE.mazUnreachableError
                                      _ -> MAlonzo.RTE.mazUnreachableError
                               _ -> MAlonzo.RTE.mazUnreachableError))))
        MAlonzo.Code.Scoped.C_constr_556 v3 v4 v5
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v3)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v6 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe d_isSOPType_436 (coe v0) (coe v6))
                       (coe
                          du_'46'extendedlambda24_1388 (coe v0) (coe v1) (coe v4) (coe v5))))
        MAlonzo.Code.Scoped.C_case_564 v3 v4 v5
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe
                  d_checkKind_554 (coe v0) (coe v3)
                  (coe MAlonzo.Code.Utils.C_'42'_654))
               (coe
                  (\ v6 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe d_inferType_1156 (coe v0) (coe v1) (coe v4))
                       (coe
                          (\ v7 ->
                             coe
                               MAlonzo.Code.Utils.du_eitherBind_42
                               (coe du_isSOP_476 (coe v0) (coe v7))
                               (coe
                                  du_'46'extendedlambda24_1410 (coe v0) (coe v1) (coe v5)
                                  (coe v6))))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.checkConstrArgs-List
  d_checkConstrArgs'45'List_1180 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    [MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4] ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Utils.List.T_IList_302
  d_checkConstrArgs'45'List_1180 v0 v1 v2 v3
    = case coe v2 of
        MAlonzo.Code.Utils.C_'91''93'_388
          -> case coe v3 of
               []
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe MAlonzo.Code.Utils.List.C_'91''93'_308)
               (:) v4 v5
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_TooFewConstrArgs_86)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Utils.C__'8759'__390 v4 v5
          -> case coe v3 of
               []
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_TooManyConstrArgs_84)
               (:) v6 v7
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe d_checkType_1148 (coe v0) (coe v1) (coe v4) (coe v6))
                      (coe
                         (\ v8 ->
                            coe
                              MAlonzo.Code.Utils.du_eitherBind_42
                              (coe
                                 d_checkConstrArgs'45'List_1180 (coe v0) (coe v1) (coe v5) (coe v7))
                              (coe
                                 (\ v9 ->
                                    coe
                                      MAlonzo.Code.Utils.C_inj'8322'_14
                                      (coe MAlonzo.Code.Utils.List.C__'8759'__314 v8 v9)))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check.checkCases-List
  d_checkCases'45'List_1220 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    Integer ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Algorithmic.T_Cases_172
  d_checkCases'45'List_1220 v0 v1 v2 v3 ~v4 v5
    = du_checkCases'45'List_1220 v0 v1 v2 v3 v5
  du_checkCases'45'List_1220 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Data.Vec.Base.T_Vec_28 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Algorithmic.T_Cases_172
  du_checkCases'45'List_1220 v0 v1 v2 v3 v4
    = case coe v3 of
        MAlonzo.Code.Utils.C_'91''93'_388
          -> case coe v4 of
               MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
                 -> coe
                      MAlonzo.Code.Utils.C_inj'8322'_14
                      (coe MAlonzo.Code.Algorithmic.C_'91''93'_278)
               MAlonzo.Code.Data.Vec.Base.C__'8759'__38 v6 v7
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_TooFewCases_88)
               _ -> MAlonzo.RTE.mazUnreachableError
        MAlonzo.Code.Utils.C__'8759'__390 v5 v6
          -> case coe v4 of
               MAlonzo.Code.Data.Vec.Base.C_'91''93'_32
                 -> coe MAlonzo.Code.Utils.C_inj'8321'_12 (coe C_TooManyCases_90)
               MAlonzo.Code.Data.Vec.Base.C__'8759'__38 v8 v9
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe
                         d_checkType_1148 (coe v0) (coe v1) (coe v5)
                         (coe MAlonzo.Code.Algorithmic.du_mkCaseType_156 v2 v8))
                      (coe
                         (\ v10 ->
                            coe
                              MAlonzo.Code.Utils.du_eitherBind_42
                              (coe
                                 du_checkCases'45'List_1220 (coe v0) (coe v1) (coe v2) (coe v6)
                                 (coe v9))
                              (coe
                                 (\ v11 ->
                                    coe
                                      MAlonzo.Code.Utils.C_inj'8322'_14
                                      (coe MAlonzo.Code.Algorithmic.C__'8759'__290 v10 v11)))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda24
  d_'46'extendedlambda24_1314 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda24_1314 v0 v1 ~v2 v3 ~v4 v5
    = du_'46'extendedlambda24_1314 v0 v1 v3 v5
  du_'46'extendedlambda24_1314 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda24_1314 v0 v1 v2 v3
    = case coe v3 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v4 v5
          -> case coe v5 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v6 v7
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe d_checkType_1148 (coe v0) (coe v1) (coe v2) (coe v4))
                      (coe
                         (\ v8 ->
                            coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v6)
                                 (coe MAlonzo.Code.Algorithmic.C__'183'__196 v4 v7 v8))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda24
  d_'46'extendedlambda24_1352 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda24_1352 v0 v1 ~v2 v3 v4 ~v5 v6
    = du_'46'extendedlambda24_1352 v0 v1 v3 v4 v6
  du_'46'extendedlambda24_1352 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda24_1352 v0 v1 v2 v3 v4
    = case coe v4 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_checkKind_554 (coe v0) (coe v2) (coe v5))
               (coe
                  (\ v7 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe
                          d_checkType_1148 (coe v0) (coe v1) (coe v3)
                          (coe
                             MAlonzo.Code.Type.BetaNBE.d_nf_258 (coe v0)
                             (coe MAlonzo.Code.Utils.C_'42'_654)
                             (coe
                                MAlonzo.Code.Type.C__'183'__30 v5
                                (coe
                                   MAlonzo.Code.Type.C__'183'__30
                                   (coe
                                      MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                      (coe MAlonzo.Code.Utils.C_'42'_654))
                                   (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                      (coe v0)
                                      (coe
                                         MAlonzo.Code.Utils.C__'8658'__658
                                         (coe
                                            MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                            (coe MAlonzo.Code.Utils.C_'42'_654))
                                         (coe
                                            MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                            (coe MAlonzo.Code.Utils.C_'42'_654)))
                                      (coe v6))
                                   (coe
                                      MAlonzo.Code.Type.C_ƛ_28
                                      (coe
                                         MAlonzo.Code.Type.C_μ_32 v5
                                         (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                            (coe MAlonzo.Code.Type.C__'44''8902'__6 (coe v0) (coe v5))
                                            (coe
                                               MAlonzo.Code.Utils.C__'8658'__658
                                               (coe
                                                  MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                                  (coe MAlonzo.Code.Utils.C_'42'_654))
                                               (coe
                                                  MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                                  (coe MAlonzo.Code.Utils.C_'42'_654)))
                                            (coe
                                               MAlonzo.Code.Type.BetaNormal.d_weakenNf_122 v0
                                               (coe
                                                  MAlonzo.Code.Utils.C__'8658'__658
                                                  (coe
                                                     MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                                     (coe MAlonzo.Code.Utils.C_'42'_654))
                                                  (coe
                                                     MAlonzo.Code.Utils.C__'8658'__658 (coe v5)
                                                     (coe MAlonzo.Code.Utils.C_'42'_654)))
                                               v5 v6))
                                         (coe
                                            MAlonzo.Code.Type.C_'96'_22
                                            (coe MAlonzo.Code.Type.C_Z_16)))))
                                (MAlonzo.Code.Type.BetaNormal.d_embNf_128
                                   (coe v0) (coe v5) (coe v7)))))
                       (coe
                          (\ v8 ->
                             coe
                               MAlonzo.Code.Utils.C_inj'8322'_14
                               (coe
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                  (coe MAlonzo.Code.Type.BetaNormal.C_μ_24 v5 v6 v7)
                                  (coe MAlonzo.Code.Algorithmic.C_wrap_220 v8))))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda24
  d_'46'extendedlambda24_1388 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    Integer ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda24_1388 v0 v1 ~v2 v3 v4 ~v5 v6
    = du_'46'extendedlambda24_1388 v0 v1 v3 v4 v6
  du_'46'extendedlambda24_1388 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    Integer ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda24_1388 v0 v1 v2 v3 v4
    = case coe v4 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
          -> coe
               MAlonzo.Code.Utils.du_eitherBind_42
               (coe d_chkIdx_514 (coe v2) (coe v5))
               (coe
                  (\ v7 ->
                     coe
                       MAlonzo.Code.Utils.du_eitherBind_42
                       (coe
                          d_checkConstrArgs'45'List_1180 (coe v0) (coe v1) (coe v3)
                          (coe MAlonzo.Code.Data.Vec.Base.du_lookup_82 (coe v6) (coe v7)))
                       (coe
                          (\ v8 ->
                             coe
                               MAlonzo.Code.Utils.C_inj'8322'_14
                               (coe
                                  MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32
                                  (coe MAlonzo.Code.Type.BetaNormal.C_SOP_28 v5 v6)
                                  (coe
                                     MAlonzo.Code.Algorithmic.C_constr_240 v7
                                     (coe MAlonzo.Code.Data.Vec.Base.du_lookup_82 (coe v6) (coe v7))
                                     v8))))))
        _ -> MAlonzo.RTE.mazUnreachableError
  -- Check..extendedlambda24
  d_'46'extendedlambda24_1410 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Scoped.T_ScopedTy_14 ->
    MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  d_'46'extendedlambda24_1410 v0 v1 ~v2 ~v3 v4 v5 ~v6 v7
    = du_'46'extendedlambda24_1410 v0 v1 v4 v5 v7
  du_'46'extendedlambda24_1410 ::
    MAlonzo.Code.Type.T_Ctx'8902'_2 ->
    MAlonzo.Code.Algorithmic.T_Ctx_2 ->
    MAlonzo.Code.Utils.T_List_384 MAlonzo.Code.Scoped.T_ScopedTm_522 ->
    MAlonzo.Code.Type.BetaNormal.T__'8866'Nf'8902'__4 ->
    MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
    MAlonzo.Code.Utils.T_Either_6
      T_TypeError_12 MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14
  du_'46'extendedlambda24_1410 v0 v1 v2 v3 v4
    = case coe v4 of
        MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v5 v6
          -> case coe v6 of
               MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 v7 v8
                 -> coe
                      MAlonzo.Code.Utils.du_eitherBind_42
                      (coe
                         du_checkCases'45'List_1220 (coe v0) (coe v1) (coe v3) (coe v2)
                         (coe v7))
                      (coe
                         (\ v9 ->
                            coe
                              MAlonzo.Code.Utils.C_inj'8322'_14
                              (coe
                                 MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 (coe v3)
                                 (coe MAlonzo.Code.Algorithmic.C_case_252 v5 v7 v8 v9))))
               _ -> MAlonzo.RTE.mazUnreachableError
        _ -> MAlonzo.RTE.mazUnreachableError
  