{-# 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.VerifiedCompilation.UCaseOfCase where

import Data.Text qualified
import MAlonzo.Code.Agda.Builtin.Sigma qualified
import MAlonzo.Code.Builtin qualified
import MAlonzo.Code.Data.Irrelevant qualified
import MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base qualified
import MAlonzo.Code.Data.Nat.Properties qualified
import MAlonzo.Code.Relation.Nullary.Decidable.Core qualified
import MAlonzo.Code.Relation.Nullary.Reflects qualified
import MAlonzo.Code.Untyped qualified
import MAlonzo.Code.VerifiedCompilation.Certificate qualified
import MAlonzo.Code.VerifiedCompilation.Equality qualified
import MAlonzo.Code.VerifiedCompilation.UntypedTranslation qualified
import MAlonzo.Code.VerifiedCompilation.UntypedViews qualified
import MAlonzo.RTE (AgdaAny, add64, addInt, coe, eq64, eqInt, erased, geqInt, lt64, ltInt, mul64,
                    mulInt, quot64, quotInt, rem64, remInt, sub64, subInt, word64FromNat,
                    word64ToNat)
import MAlonzo.RTE qualified

-- VerifiedCompilation.UCaseOfCase.CoC
d_CoC_4 :: p -> p -> p -> p -> ()
d_CoC_4 p
a0 p
a1 p
a2 p
a3 = ()
data T_CoC_4
  = C_isCoC_28 MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
               MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48
-- VerifiedCompilation.UCaseOfCase.CaseOfCase
d_CaseOfCase_38 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 -> ()
d_CaseOfCase_38 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
d_CaseOfCase_38 = () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> ()
forall a. a
erased
-- VerifiedCompilation.UCaseOfCase.CoCCase
d_CoCCase_42 :: p -> p -> ()
d_CoCCase_42 p
a0 p
a1 = ()
data T_CoCCase_42 = C_isCoCCase_58
-- VerifiedCompilation.UCaseOfCase.isCoCCase?
d_isCoCCase'63'_62 ::
  () ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isCoCCase'63'_62 :: () -> T__'8866'_14 -> T_Dec_20
d_isCoCCase'63'_62 ~()
v0 T__'8866'_14
v1 = T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 T__'8866'_14
v1
du_isCoCCase'63'_62 ::
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isCoCCase'63'_62 :: T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 T__'8866'_14
v0
  = let v1 :: Any
v1
          = (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> [T__'8866'_14] -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any -> Any
forall a b. a -> b
coe
              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isCase'63'_598
              Any
forall a. a
erased
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v1 ->
                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                      Any
forall a. a
erased
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v2 ->
                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                              Any
forall a. a
erased
                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                 (\ Any
v3 ->
                                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                      ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                                      Any
forall a. a
erased
                                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                                         (\ Any
v4 ->
                                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                              () -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isForce'63'_284
                                              Any
forall a. a
erased
                                              (\ Any
v5 Any
v6 ->
                                                 (T__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                                   T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isBuiltin'63'_708
                                                   Any
v6)))
                                      (\ Any
v4 Any
v5 ->
                                         T_Dec_20 -> Any
forall a b. a -> b
coe
                                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                 (\ Any
v3 ->
                                    (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                      ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                                      Any
forall a. a
erased
                                      (\ Any
v4 Any
v5 ->
                                         T_Dec_20 -> Any
forall a b. a -> b
coe
                                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v2 ->
                            (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                              ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                              Any
forall a. a
erased
                              (\ Any
v3 Any
v4 ->
                                 T_Dec_20 -> Any
forall a b. a -> b
coe
                                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))
              (\ Any
v1 Any
v2 ->
                 T_Dec_20 -> Any
forall a b. a -> b
coe
                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)
              (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v0) in
    Any -> T_Dec_20
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
v1 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v2 T_Reflects_16
v3
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v2
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v3 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v4
                         -> case Any -> T_isCase_574
forall a b. a -> b
coe Any
v4 of
                              MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v7 Any
v8
                                -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v0 of
                                     MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v9 [T__'8866'_14]
v10
                                       -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v7 of
                                            MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v13 Any
v14
                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9 of
                                                   MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v15 T__'8866'_14
v16
                                                     -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v13 of
                                                          MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v19 Any
v20
                                                            -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v15 of
                                                                 MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v21 T__'8866'_14
v22
                                                                   -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v19 of
                                                                        MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v25 Any
v26
                                                                          -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v21 of
                                                                               MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v27 T__'8866'_14
v28
                                                                                 -> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v25 of
                                                                                      MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v30
                                                                                        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                  T__'8866'_14
v27 of
                                                                                             MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v31
                                                                                               -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                    Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                    (Any -> Any
forall a b. a -> b
coe
                                                                                                       Any
v30)
                                                                                                    (case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                            T__'8866'_14
v31 of
                                                                                                       MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v32
                                                                                                         -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                              Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                              (Any -> Any
forall a b. a -> b
coe
                                                                                                                 Any
v26)
                                                                                                              (case Any -> T_isConstr_478
forall a b. a -> b
coe
                                                                                                                      Any
v20 of
                                                                                                                 MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v35
                                                                                                                   -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                        Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                        (Any -> Any
forall a b. a -> b
coe
                                                                                                                           Any
v35)
                                                                                                                        (case Any -> T_isConstr_478
forall a b. a -> b
coe
                                                                                                                                Any
v14 of
                                                                                                                           MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v38
                                                                                                                             -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                  Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                  (Any -> Any
forall a b. a -> b
coe
                                                                                                                                     Any
v38)
                                                                                                                                  ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                     Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                     (Any -> Any
forall a b. a -> b
coe
                                                                                                                                        Any
v8)
                                                                                                                                     (let v39 :: T_Dec_20
v39
                                                                                                                                            = T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_404
                                                                                                                                                (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe
                                                                                                                                                   T_Builtin_2
v32)
                                                                                                                                                (T_Builtin_2 -> T_Builtin_2
forall a b. a -> b
coe
                                                                                                                                                   T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60) in
                                                                                                                                      Any -> Any
forall a b. a -> b
coe
                                                                                                                                        (case T_Dec_20 -> T_Dec_20
forall a b. a -> b
coe
                                                                                                                                                T_Dec_20
v39 of
                                                                                                                                           MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v40 T_Reflects_16
v41
                                                                                                                                             -> if Bool -> Bool
forall a b. a -> b
coe
                                                                                                                                                     Bool
v40
                                                                                                                                                  then (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                         Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                         (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                            T_Reflects_16
v41)
                                                                                                                                                         ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                            Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                                                                                                                            (Bool -> Any
forall a b. a -> b
coe
                                                                                                                                                               Bool
v40)
                                                                                                                                                            ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                               Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                                                                                                                               (T_CoCCase_42 -> Any
forall a b. a -> b
coe
                                                                                                                                                                  T_CoCCase_42
C_isCoCCase_58)))
                                                                                                                                                  else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                         Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                         (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                            T_Reflects_16
v41)
                                                                                                                                                         ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                            Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                                                                                                                            (Bool -> Any
forall a b. a -> b
coe
                                                                                                                                                               Bool
v40)
                                                                                                                                                            (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                               T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                                                                                                                                           T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
                                                                                                                           T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                                 T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                       T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                             T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                      T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                               T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                        T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                 T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                          T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                            T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v3)
                       ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                          (Bool -> Any
forall a b. a -> b
coe Bool
v2)
                          (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCaseOfCase.CoCForce
d_CoCForce_146 :: p -> p -> ()
d_CoCForce_146 p
a0 p
a1 = ()
data T_CoCForce_146 = C_isCoCForce_162
-- VerifiedCompilation.UCaseOfCase.isCoCForce?
d_isCoCForce'63'_168 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
d_isCoCForce'63'_168 :: () -> T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
d_isCoCForce'63'_168 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 = T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 T_DecEq_6
v1 T__'8866'_14
v2
du_isCoCForce'63'_168 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Relation.Nullary.Decidable.Core.T_Dec_20
du_isCoCForce'63'_168 :: T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 T_DecEq_6
v0 T__'8866'_14
v1
  = let v2 :: Any
v2
          = (()
 -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
              () -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isForce'63'_284
              Any
forall a. a
erased
              ((Any -> Any) -> Any
forall a b. a -> b
coe
                 (\ Any
v2 ->
                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                      ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                      Any
forall a. a
erased
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v3 ->
                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                              Any
forall a. a
erased
                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                 (\ Any
v4 ->
                                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                      ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> T__'8866'_14 -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isApp'63'_166
                                      Any
forall a. a
erased
                                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                                         (\ Any
v5 ->
                                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                              () -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isForce'63'_284
                                              Any
forall a. a
erased
                                              (\ Any
v6 Any
v7 ->
                                                 (T__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe
                                                   T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isBuiltin'63'_708
                                                   Any
v7)))
                                      (\ Any
v5 Any
v6 ->
                                         T_Dec_20 -> Any
forall a b. a -> b
coe
                                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isTerm'63'_782)))
                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                 (\ Any
v4 ->
                                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                      () -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_370
                                      Any
forall a. a
erased
                                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                                         (\ Any
v5 ->
                                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> [T__'8866'_14] -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                              ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isCase'63'_598
                                              Any
forall a. a
erased
                                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                                 (\ Any
v6 ->
                                                    (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                                      ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                                                      Any
forall a. a
erased
                                                      (\ Any
v7 Any
v8 ->
                                                         T_Dec_20 -> Any
forall a b. a -> b
coe
                                                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
                                              (\ Any
v6 Any
v7 ->
                                                 T_Dec_20 -> Any
forall a b. a -> b
coe
                                                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))))
                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                         (\ Any
v3 ->
                            (()
 -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> Any -> Any
forall a b. a -> b
coe
                              () -> (() -> T__'8866'_14 -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isDelay'63'_370
                              Any
forall a. a
erased
                              ((Any -> Any) -> Any
forall a b. a -> b
coe
                                 (\ Any
v4 ->
                                    (()
 -> (() -> T__'8866'_14 -> T_Dec_20)
 -> (() -> [T__'8866'_14] -> T_Dec_20)
 -> T__'8866'_14
 -> T_Dec_20)
-> Any -> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                      ()
-> (() -> T__'8866'_14 -> T_Dec_20)
-> (() -> [T__'8866'_14] -> T_Dec_20)
-> T__'8866'_14
-> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isCase'63'_598
                                      Any
forall a. a
erased
                                      ((Any -> Any) -> Any
forall a b. a -> b
coe
                                         (\ Any
v5 ->
                                            (()
 -> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20)
-> Any -> (Any -> Any -> Any) -> Any
forall a b. a -> b
coe
                                              ()
-> (() -> [T__'8866'_14] -> T_Dec_20) -> T__'8866'_14 -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_isConstr'63'_496
                                              Any
forall a. a
erased
                                              (\ Any
v6 Any
v7 ->
                                                 T_Dec_20 -> Any
forall a b. a -> b
coe
                                                   T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))
                                      (\ Any
v5 Any
v6 ->
                                         T_Dec_20 -> Any
forall a b. a -> b
coe
                                           T_Dec_20
MAlonzo.Code.VerifiedCompilation.UntypedViews.du_allTerms'63'_798)))))))
              (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1) in
    Any -> T_Dec_20
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
v2 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v3 T_Reflects_16
v4
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v3
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v4 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v5
                         -> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v5 of
                              MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v7
                                -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                                     MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v8
                                       -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v7 of
                                            MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v11 Any
v12
                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v8 of
                                                   MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v13 T__'8866'_14
v14
                                                     -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v11 of
                                                          MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v17 Any
v18
                                                            -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v13 of
                                                                 MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v19 T__'8866'_14
v20
                                                                   -> case Any -> T_isApp_142
forall a b. a -> b
coe Any
v17 of
                                                                        MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isapp_154 Any
v23 Any
v24
                                                                          -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v19 of
                                                                               MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v25 T__'8866'_14
v26
                                                                                 -> case Any -> T_isForce_268
forall a b. a -> b
coe Any
v23 of
                                                                                      MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isforce_276 Any
v28
                                                                                        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                  T__'8866'_14
v25 of
                                                                                             MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v29
                                                                                               -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                    Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                    (Any -> Any
forall a b. a -> b
coe
                                                                                                       Any
v28)
                                                                                                    (case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                            T__'8866'_14
v29 of
                                                                                                       MAlonzo.Code.Untyped.C_builtin_44 T_Builtin_2
v30
                                                                                                         -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                              Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                              (Any -> Any
forall a b. a -> b
coe
                                                                                                                 Any
v24)
                                                                                                              (case Any -> T_isDelay_354
forall a b. a -> b
coe
                                                                                                                      Any
v18 of
                                                                                                                 MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v32
                                                                                                                   -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                             T__'8866'_14
v20 of
                                                                                                                        MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v33
                                                                                                                          -> case Any -> T_isCase_574
forall a b. a -> b
coe
                                                                                                                                    Any
v32 of
                                                                                                                               MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v36 Any
v37
                                                                                                                                 -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                           T__'8866'_14
v33 of
                                                                                                                                      MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v38 [T__'8866'_14]
v39
                                                                                                                                        -> case Any -> T_isConstr_478
forall a b. a -> b
coe
                                                                                                                                                  Any
v36 of
                                                                                                                                             MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v42
                                                                                                                                               -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                    Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                    (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                       Any
v42)
                                                                                                                                                    ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                       Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                       (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                          Any
v37)
                                                                                                                                                       (case Any -> T_isDelay_354
forall a b. a -> b
coe
                                                                                                                                                               Any
v12 of
                                                                                                                                                          MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isdelay_362 Any
v44
                                                                                                                                                            -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                                                      T__'8866'_14
v14 of
                                                                                                                                                                 MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v45
                                                                                                                                                                   -> case Any -> T_isCase_574
forall a b. a -> b
coe
                                                                                                                                                                             Any
v44 of
                                                                                                                                                                        MAlonzo.Code.VerifiedCompilation.UntypedViews.C_iscase_586 Any
v48 Any
v49
                                                                                                                                                                          -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                                                                    T__'8866'_14
v45 of
                                                                                                                                                                               MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v50 [T__'8866'_14]
v51
                                                                                                                                                                                 -> case Any -> T_isConstr_478
forall a b. a -> b
coe
                                                                                                                                                                                           Any
v48 of
                                                                                                                                                                                      MAlonzo.Code.VerifiedCompilation.UntypedViews.C_isconstr_488 Any
v54
                                                                                                                                                                                        -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                                             (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                Any
v54)
                                                                                                                                                                                             ((Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                                                (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   Any
v49)
                                                                                                                                                                                                (let v55 :: Any
v55
                                                                                                                                                                                                       = (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                           T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                                                                                                                                                                                                           ((T_Builtin_2 -> T_Builtin_2 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                              T_Builtin_2 -> T_Builtin_2 -> T_Dec_20
MAlonzo.Code.Builtin.d_decBuiltin_404
                                                                                                                                                                                                              (T_Builtin_2 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                 T_Builtin_2
v30)
                                                                                                                                                                                                              (T_Builtin_2 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                 T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60))
                                                                                                                                                                                                           ((T_DecEq_6 -> Any -> Any -> T_Dec_20)
-> Any -> [T__'8866'_14] -> [T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                              T_DecEq_6 -> Any -> Any -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12
                                                                                                                                                                                                              ((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                 T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45'List'45''8866'_144
                                                                                                                                                                                                                 (T_DecEq_6 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                    T_DecEq_6
v0))
                                                                                                                                                                                                              [T__'8866'_14]
v39
                                                                                                                                                                                                              [T__'8866'_14]
v51) in
                                                                                                                                                                                                 Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                   (case Any -> T_Dec_20
forall a b. a -> b
coe
                                                                                                                                                                                                           Any
v55 of
                                                                                                                                                                                                      MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v56 T_Reflects_16
v57
                                                                                                                                                                                                        -> if Bool -> Bool
forall a b. a -> b
coe
                                                                                                                                                                                                                Bool
v56
                                                                                                                                                                                                             then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
                                                                                                                                                                                                                         T_Reflects_16
v57 of
                                                                                                                                                                                                                    MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v58
                                                                                                                                                                                                                      -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                                                                           (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              Any
v58)
                                                                                                                                                                                                                           ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                                                                                                                                                                                              (Bool -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 Bool
v56)
                                                                                                                                                                                                                              ((Any -> T_Reflects_16) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                 Any -> T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22
                                                                                                                                                                                                                                 (T_CoCForce_146 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                                    T_CoCForce_146
C_isCoCForce_162)))
                                                                                                                                                                                                                    T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                                                             else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                    Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                                                                    (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                       T_Reflects_16
v57)
                                                                                                                                                                                                                    ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                       Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                                                                                                                                                                                                                       (Bool -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                          Bool
v56)
                                                                                                                                                                                                                       (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                          T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
                                                                                                                                                                                                      T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)))
                                                                                                                                                                                      T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                               T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                        T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                 T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                          T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                                                                                                                             T_isConstr_478
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                      T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                               T_isCase_574
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                        T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                 T_isDelay_354
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                       T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                             T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                      T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                               T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                        T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                 T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                          T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                            T_isApp_142
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                              T_isForce_268
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v4)
                       ((Bool -> T_Reflects_16 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                          Bool -> T_Reflects_16 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32
                          (Bool -> Any
forall a b. a -> b
coe Bool
v3)
                          (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
MAlonzo.Code.Relation.Nullary.Reflects.C_of'8319'_26))
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCaseOfCase.isCaseOfCase?
d_isCaseOfCase'63'_264 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCaseOfCase'63'_264 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCaseOfCase'63'_264 ~()
v0 T_DecEq_6
v1 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseOfCase'63'_264 T_DecEq_6
v1
du_isCaseOfCase'63'_264 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCaseOfCase'63'_264 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseOfCase'63'_264 T_DecEq_6
v0
  = (()
 -> T_DecEq_6
 -> T_SimplifierTag_4
 -> (()
     -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
 -> T__'8866'_14
 -> T__'8866'_14
 -> T_ProofOrCE_26)
-> Any
-> Any
-> Any
-> (Any -> Any -> Any -> Any -> Any)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
forall a b. a -> b
coe
      ()
-> T_DecEq_6
-> T_SimplifierTag_4
-> (()
    -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> T__'8866'_14
-> T__'8866'_14
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.UntypedTranslation.du_translation'63'_178
      Any
forall a. a
erased (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0)
      (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
      (\ Any
v1 Any
v2 Any
v3 Any
v4 -> (T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCoC'63'_274 Any
v2 Any
v3 Any
v4)
-- VerifiedCompilation.UCaseOfCase.isCoC?
d_isCoC'63'_274 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
d_isCoC'63'_274 :: () -> T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
d_isCoC'63'_274 ~()
v0 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3 = T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCoC'63'_274 T_DecEq_6
v1 T__'8866'_14
v2 T__'8866'_14
v3
du_isCoC'63'_274 ::
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_ProofOrCE_26
du_isCoC'63'_274 :: T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCoC'63'_274 T_DecEq_6
v0 T__'8866'_14
v1 T__'8866'_14
v2
  = let v3 :: Any
v3
          = (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
              T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
              ((T__'8866'_14 -> T_Dec_20) -> Any -> Any
forall a b. a -> b
coe T__'8866'_14 -> T_Dec_20
du_isCoCCase'63'_62 (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v1))
              ((T_DecEq_6 -> T__'8866'_14 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe T_DecEq_6 -> T__'8866'_14 -> T_Dec_20
du_isCoCForce'63'_168 (T_DecEq_6 -> Any
forall a b. a -> b
coe T_DecEq_6
v0) (T__'8866'_14 -> Any
forall a b. a -> b
coe T__'8866'_14
v2)) in
    Any -> T_ProofOrCE_26
forall a b. a -> b
coe
      (case Any -> T_Dec_20
forall a b. a -> b
coe Any
v3 of
         MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v4 T_Reflects_16
v5
           -> if Bool -> Bool
forall a b. a -> b
coe Bool
v4
                then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe T_Reflects_16
v5 of
                       MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v6
                         -> case Any -> T_Σ_14
forall a b. a -> b
coe Any
v6 of
                              MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v7 Any
v8
                                -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                     Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v7)
                                     (case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v1 of
                                        MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v9 [T__'8866'_14]
v10
                                          -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v9 of
                                               MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v11 T__'8866'_14
v12
                                                 -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v11 of
                                                      MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v13 T__'8866'_14
v14
                                                        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v13 of
                                                             MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v15 T__'8866'_14
v16
                                                               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v14 of
                                                                    MAlonzo.Code.Untyped.C_constr_34 Integer
v17 [T__'8866'_14]
v18
                                                                      -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v12 of
                                                                           MAlonzo.Code.Untyped.C_constr_34 Integer
v19 [T__'8866'_14]
v20
                                                                             -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                  Any -> Any -> Any
forall a b. a -> b -> b
seq (Any -> Any
forall a b. a -> b
coe Any
v8)
                                                                                  (case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe T__'8866'_14
v2 of
                                                                                     MAlonzo.Code.Untyped.C_force_24 T__'8866'_14
v21
                                                                                       -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                 T__'8866'_14
v21 of
                                                                                            MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v22 T__'8866'_14
v23
                                                                                              -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                        T__'8866'_14
v22 of
                                                                                                   MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v24 T__'8866'_14
v25
                                                                                                     -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                               T__'8866'_14
v24 of
                                                                                                          MAlonzo.Code.Untyped.C__'183'__22 T__'8866'_14
v26 T__'8866'_14
v27
                                                                                                            -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                      T__'8866'_14
v25 of
                                                                                                                 MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v28
                                                                                                                   -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                             T__'8866'_14
v28 of
                                                                                                                        MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v29 [T__'8866'_14]
v30
                                                                                                                          -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                    T__'8866'_14
v29 of
                                                                                                                               MAlonzo.Code.Untyped.C_constr_34 Integer
v31 [T__'8866'_14]
v32
                                                                                                                                 -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                           T__'8866'_14
v23 of
                                                                                                                                      MAlonzo.Code.Untyped.C_delay_26 T__'8866'_14
v33
                                                                                                                                        -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                                  T__'8866'_14
v33 of
                                                                                                                                             MAlonzo.Code.Untyped.C_case_40 T__'8866'_14
v34 [T__'8866'_14]
v35
                                                                                                                                               -> case T__'8866'_14 -> T__'8866'_14
forall a b. a -> b
coe
                                                                                                                                                         T__'8866'_14
v34 of
                                                                                                                                                    MAlonzo.Code.Untyped.C_constr_34 Integer
v36 [T__'8866'_14]
v37
                                                                                                                                                      -> let v38 :: Any
v38
                                                                                                                                                               = (T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                   T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                                                                                                                                                                   ((T_DecEq_6 -> Any -> Any -> T_Dec_20)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                      T_DecEq_6 -> Any -> Any -> T_Dec_20
MAlonzo.Code.VerifiedCompilation.Equality.d__'8799'__12
                                                                                                                                                                      ((T_DecEq_6 -> T_DecEq_6) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                         T_DecEq_6 -> T_DecEq_6
MAlonzo.Code.VerifiedCompilation.Equality.du_DecEq'45''8866'_138
                                                                                                                                                                         (T_DecEq_6 -> Any
forall a b. a -> b
coe
                                                                                                                                                                            T_DecEq_6
v0))
                                                                                                                                                                      T__'8866'_14
v16
                                                                                                                                                                      T__'8866'_14
v27)
                                                                                                                                                                   ((T_Dec_20 -> T_Dec_20 -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                      T_Dec_20 -> T_Dec_20 -> T_Dec_20
MAlonzo.Code.Relation.Nullary.Decidable.Core.du__'215''45'dec__76
                                                                                                                                                                      ((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                         Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
                                                                                                                                                                         (Integer -> Any
forall a b. a -> b
coe
                                                                                                                                                                            Integer
v17)
                                                                                                                                                                         (Integer -> Any
forall a b. a -> b
coe
                                                                                                                                                                            Integer
v31))
                                                                                                                                                                      ((Integer -> Integer -> T_Dec_20) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                         Integer -> Integer -> T_Dec_20
MAlonzo.Code.Data.Nat.Properties.d__'8799'__2688
                                                                                                                                                                         (Integer -> Any
forall a b. a -> b
coe
                                                                                                                                                                            Integer
v19)
                                                                                                                                                                         (Integer -> Any
forall a b. a -> b
coe
                                                                                                                                                                            Integer
v36))) in
                                                                                                                                                         Any -> Any
forall a b. a -> b
coe
                                                                                                                                                           (case Any -> T_Dec_20
forall a b. a -> b
coe
                                                                                                                                                                   Any
v38 of
                                                                                                                                                              MAlonzo.Code.Relation.Nullary.Decidable.Core.C__because__32 Bool
v39 T_Reflects_16
v40
                                                                                                                                                                -> if Bool -> Bool
forall a b. a -> b
coe
                                                                                                                                                                        Bool
v39
                                                                                                                                                                     then case T_Reflects_16 -> T_Reflects_16
forall a b. a -> b
coe
                                                                                                                                                                                 T_Reflects_16
v40 of
                                                                                                                                                                            MAlonzo.Code.Relation.Nullary.Reflects.C_of'696'_22 Any
v41
                                                                                                                                                                              -> case Any -> T_Σ_14
forall a b. a -> b
coe
                                                                                                                                                                                        Any
v41 of
                                                                                                                                                                                   MAlonzo.Code.Agda.Builtin.Sigma.C__'44'__32 Any
v42 Any
v43
                                                                                                                                                                                     -> (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                          Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                                          (Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             Any
v43)
                                                                                                                                                                                          (let v44 :: Any
v44
                                                                                                                                                                                                 = (T_SimplifierTag_4
 -> (Any -> Any -> T_ProofOrCE_26)
 -> [Any]
 -> [Any]
 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                     T_SimplifierTag_4
-> (Any -> Any -> T_ProofOrCE_26)
-> [Any]
-> [Any]
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_140
                                                                                                                                                                                                     (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                        T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
                                                                                                                                                                                                     ((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                        T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseOfCase'63'_264
                                                                                                                                                                                                        (T_DecEq_6 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                           T_DecEq_6
v0))
                                                                                                                                                                                                     ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                        [T__'8866'_14]
v18)
                                                                                                                                                                                                     ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                        [T__'8866'_14]
v32) in
                                                                                                                                                                                           Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                             (case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
                                                                                                                                                                                                     Any
v44 of
                                                                                                                                                                                                MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v45
                                                                                                                                                                                                  -> let v46 :: Any
v46
                                                                                                                                                                                                           = (T_SimplifierTag_4
 -> (Any -> Any -> T_ProofOrCE_26)
 -> [Any]
 -> [Any]
 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                               T_SimplifierTag_4
-> (Any -> Any -> T_ProofOrCE_26)
-> [Any]
-> [Any]
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_140
                                                                                                                                                                                                               (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
                                                                                                                                                                                                               ((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseOfCase'63'_264
                                                                                                                                                                                                                  (T_DecEq_6 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                     T_DecEq_6
v0))
                                                                                                                                                                                                               ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  [T__'8866'_14]
v20)
                                                                                                                                                                                                               ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                  [T__'8866'_14]
v37) in
                                                                                                                                                                                                     Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                       (case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
                                                                                                                                                                                                               Any
v46 of
                                                                                                                                                                                                          MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v47
                                                                                                                                                                                                            -> let v48 :: Any
v48
                                                                                                                                                                                                                     = (T_SimplifierTag_4
 -> (Any -> Any -> T_ProofOrCE_26)
 -> [Any]
 -> [Any]
 -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                         T_SimplifierTag_4
-> (Any -> Any -> T_ProofOrCE_26)
-> [Any]
-> [Any]
-> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.du_pcePointwise_140
                                                                                                                                                                                                                         (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                            T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
                                                                                                                                                                                                                         ((T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26)
-> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                            T_DecEq_6 -> T__'8866'_14 -> T__'8866'_14 -> T_ProofOrCE_26
du_isCaseOfCase'63'_264
                                                                                                                                                                                                                            (T_DecEq_6 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                               T_DecEq_6
v0))
                                                                                                                                                                                                                         ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                            [T__'8866'_14]
v10)
                                                                                                                                                                                                                         ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                            [T__'8866'_14]
v30) in
                                                                                                                                                                                                               Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                 (case Any -> T_ProofOrCE_26
forall a b. a -> b
coe
                                                                                                                                                                                                                         Any
v48 of
                                                                                                                                                                                                                    MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32 Any
v49
                                                                                                                                                                                                                      -> (Any -> T_ProofOrCE_26) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_proof_32
                                                                                                                                                                                                                           ((T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 -> T_CoC_4)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                              T_Pointwise_48 -> T_Pointwise_48 -> T_Pointwise_48 -> T_CoC_4
C_isCoC_28
                                                                                                                                                                                                                              Any
v49
                                                                                                                                                                                                                              Any
v45
                                                                                                                                                                                                                              Any
v47)
                                                                                                                                                                                                                    MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v52 Any
v53 Any
v54
                                                                                                                                                                                                                      -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                           T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                                                                                                                                                           T_SimplifierTag_4
v52
                                                                                                                                                                                                                           Any
v53
                                                                                                                                                                                                                           Any
v54
                                                                                                                                                                                                                    T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                                                                                                                          MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v50 Any
v51 Any
v52
                                                                                                                                                                                                            -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                                 T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                                                                                                                                                 T_SimplifierTag_4
v50
                                                                                                                                                                                                                 Any
v51
                                                                                                                                                                                                                 Any
v52
                                                                                                                                                                                                          T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                                                                                                                MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40 T_SimplifierTag_4
v48 Any
v49 Any
v50
                                                                                                                                                                                                  -> (T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> T_SimplifierTag_4 -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                       T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                                                                                                                                       T_SimplifierTag_4
v48
                                                                                                                                                                                                       Any
v49
                                                                                                                                                                                                       Any
v50
                                                                                                                                                                                                T_ProofOrCE_26
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError))
                                                                                                                                                                                   T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                            T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                                                     else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                            Any -> Any -> Any
forall a b. a -> b -> b
seq
                                                                                                                                                                            (T_Reflects_16 -> Any
forall a b. a -> b
coe
                                                                                                                                                                               T_Reflects_16
v40)
                                                                                                                                                                            ((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                               T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                                                                                                                                                                               (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                  T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
                                                                                                                                                                               ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                  T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
                                                                                                                                                                                  ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                     T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                     ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                        T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                        ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                           T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                           ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
                                                                                                                                                                                              ((T_Builtin_2 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                 T_Builtin_2 -> T__'8866'_14
MAlonzo.Code.Untyped.C_builtin_44
                                                                                                                                                                                                 (T_Builtin_2 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                    T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60)))
                                                                                                                                                                                           (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              T__'8866'_14
v16))
                                                                                                                                                                                        (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                           T__'8866'_14
v14))
                                                                                                                                                                                     (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                        T__'8866'_14
v12))
                                                                                                                                                                                  ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                     [T__'8866'_14]
v10))
                                                                                                                                                                               ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                  T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
                                                                                                                                                                                  ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                     T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                     ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                        T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                        ((T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14) -> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                           T__'8866'_14 -> T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C__'183'__22
                                                                                                                                                                                           ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_force_24
                                                                                                                                                                                              ((T_Builtin_2 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                 T_Builtin_2 -> T__'8866'_14
MAlonzo.Code.Untyped.C_builtin_44
                                                                                                                                                                                                 (T_Builtin_2 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                                    T_Builtin_2
MAlonzo.Code.Builtin.C_ifThenElse_60)))
                                                                                                                                                                                           (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              T__'8866'_14
v27))
                                                                                                                                                                                        (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                           T__'8866'_14
v25))
                                                                                                                                                                                     ((T__'8866'_14 -> T__'8866'_14) -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                        T__'8866'_14 -> T__'8866'_14
MAlonzo.Code.Untyped.C_delay_26
                                                                                                                                                                                        ((T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14)
-> Any -> Any -> Any
forall a b. a -> b
coe
                                                                                                                                                                                           T__'8866'_14 -> [T__'8866'_14] -> T__'8866'_14
MAlonzo.Code.Untyped.C_case_40
                                                                                                                                                                                           (T__'8866'_14 -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              T__'8866'_14
v34)
                                                                                                                                                                                           ([T__'8866'_14] -> Any
forall a b. a -> b
coe
                                                                                                                                                                                              [T__'8866'_14]
v30))))))
                                                                                                                                                              T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                                                                                                    T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                             T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                                      T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                               T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                        T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                                 T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                          T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                                   T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                            T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                                     T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                                                                           T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                                    T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                             T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                                      T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                               T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                                        T__'8866'_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
                              T_Σ_14
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                       T_Reflects_16
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError
                else (Any -> Any -> Any) -> Any -> Any -> Any
forall a b. a -> b
coe
                       Any -> Any -> Any
forall a b. a -> b -> b
seq (T_Reflects_16 -> Any
forall a b. a -> b
coe T_Reflects_16
v5)
                       ((T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26)
-> Any -> T__'8866'_14 -> T__'8866'_14 -> Any
forall a b. a -> b
coe
                          T_SimplifierTag_4 -> Any -> Any -> T_ProofOrCE_26
MAlonzo.Code.VerifiedCompilation.Certificate.C_ce_40
                          (T_SimplifierTag_4 -> Any
forall a b. a -> b
coe T_SimplifierTag_4
MAlonzo.Code.VerifiedCompilation.Certificate.C_caseOfCaseT_10)
                          T__'8866'_14
v1 T__'8866'_14
v2)
         T_Dec_20
_ -> Any
forall a. a
MAlonzo.RTE.mazUnreachableError)
-- VerifiedCompilation.UCaseOfCase..extendedlambda4
d_'46'extendedlambda4_290 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda4_290 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda4_290 = ()
-> T_DecEq_6
-> T__'8866'_14
-> T__'8866'_14
-> (T_Σ_14 -> T_Irrelevant_20)
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseOfCase..extendedlambda5
d_'46'extendedlambda5_378 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  Integer ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  Integer ->
  (MAlonzo.Code.Agda.Builtin.Sigma.T_Σ_14 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda5_378 :: ()
-> T_DecEq_6
-> T__'8866'_14
-> Integer
-> Integer
-> T__'8866'_14
-> Integer
-> Integer
-> (T_Σ_14 -> T_Irrelevant_20)
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda5_378 = ()
-> T_DecEq_6
-> T__'8866'_14
-> Integer
-> Integer
-> T__'8866'_14
-> Integer
-> Integer
-> (T_Σ_14 -> T_Irrelevant_20)
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseOfCase..extendedlambda6
d_'46'extendedlambda6_454 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  (MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  AgdaAny ->
  AgdaAny ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda6_454 :: ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda6_454 = ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseOfCase..extendedlambda7
d_'46'extendedlambda7_534 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  (MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  Integer ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda7_534 :: ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda7_534 = ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> T__'8866'_14
-> Integer
-> Integer
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased
-- VerifiedCompilation.UCaseOfCase..extendedlambda8
d_'46'extendedlambda8_618 ::
  () ->
  MAlonzo.Code.VerifiedCompilation.Equality.T_DecEq_6 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  (MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
   MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20) ->
  () ->
  () ->
  MAlonzo.Code.VerifiedCompilation.Certificate.T_SimplifierTag_4 ->
  AgdaAny ->
  AgdaAny ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  [MAlonzo.Code.Untyped.T__'8866'_14] ->
  MAlonzo.Code.Data.List.Relation.Binary.Pointwise.Base.T_Pointwise_48 ->
  MAlonzo.Code.Untyped.T__'8866'_14 ->
  Integer ->
  Integer -> T_CoC_4 -> MAlonzo.Code.Data.Irrelevant.T_Irrelevant_20
d_'46'extendedlambda8_618 :: ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> T__'8866'_14
-> Integer
-> Integer
-> T_CoC_4
-> T_Irrelevant_20
d_'46'extendedlambda8_618 = ()
-> T_DecEq_6
-> [T__'8866'_14]
-> [T__'8866'_14]
-> (T_Pointwise_48 -> T_Irrelevant_20)
-> ()
-> ()
-> T_SimplifierTag_4
-> Any
-> Any
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> [T__'8866'_14]
-> [T__'8866'_14]
-> T_Pointwise_48
-> T__'8866'_14
-> Integer
-> Integer
-> T_CoC_4
-> T_Irrelevant_20
forall a. a
erased