js.v

Definition decidable (P: Prop) := {P} + {~P}.
Definition eq_dec T := forall (x y:T), decidable (x=y).

Inductive spec_type: Set :=
| abruption
| additiveExpression
| argumentList
| arguments
| arrayAssignmentPattern
| arrayBindingPattern
| arrayLiteral
| assignmentElement
| assignmentElementList
| assignmentElisionElement
| assignmentExpression
| assignmentOperator
| assignmentPattern
| assignmentProperty
| assignmentPropertyList
| assignmentRestElement
| assignmentRestProperty
| bindingElement
| bindingElementList
| bindingElisionElement
| bindingIdentifier
| bindingList
| bindingPattern
| bindingProperty
| bindingPropertyList
| bindingRestElement
| bindingRestProperty
| bindingStatus
| bitwiseANDExpression
| bitwiseORExpression
| bitwiseXORExpression
| block
| blockStatement
| booleanLiteral
| breakStatement
| breakableStatement
| callExpression
| callMemberExpression
| coalesceExpression
| coalesceExpressionHead
| codeEvaluationState
| completionType
| completionValue
| computationFlow
| computedPropertyName
| conditionalExpression
| constructorKind
| continueStatement
| coverCallExpressionAndAsyncArrowHead
| coverInitializedName
| coverParenthesizedExpressionAndArrowParameterList
| declaration
| destructuringAssignmentTarget
| elementList
| elision
| equalityExpression
| exponentiationExpression
| expression
| expressionStatement
| forBinding
| forDeclaration
| formalParameter
| formalParameterList
| formalParameters
| functionBody
| functionDeclaration
| functionExpression
| functionMode
| functionRestParameter
| functionStatementList
| hoistableDeclaration
| identifier
| identifierReference
| ifStatement
| importCall
| importMeta
| initializer
| integrityLevel
| internalSlot
| intrinsicObject
| iterationStatement
| labelIdentifier
| labelledItem
| labelledStatement
| leftHandSideExpression
| letOrConst
| lexicalBinding
| lexicalDeclaration
| lexicalEnvironment
| lexical_this
| literal
| literalPropertyName
| loc_Object
| loc_scriptOrModule
| logicalANDExpression
| logicalORExpression
| maybeEmpty
| maybeNull
| maybeUndefined
| memberExpression
| metaProperty
| multiplicativeExpression
| multiplicativeOperator
| mutability
| newExpression
| newTarget
| nullLiteral
| numericLiteral
| objectAssignmentPattern
| objectBindingPattern
| objectLiteral
| optionalChain
| optionalExpression
| out
| parenthesizedExpression
| pd_Properties
| primaryExpression
| primitivePreference
| propertyDefinition
| propertyDefinitionList
| propertyName
| reference_bv
| relationalExpression
| returnStatement
| script
| scriptBody
| shiftExpression
| shortCircuitExpression
| singleNameBinding
| spreadElement
| statement
| statementList
| statementListItem
| superCall
| superProperty
| sync
| thisBindingStatus
| throwStatement
| type_DeclarativeEnvironmentRecord
| type_EnvironmentRecord
| type_exoticInternalMethod
| type_internalMethod
| type_maybeEmpty
| type_maybeNull
| type_maybeUndefined
| type_reference
| type_valref
| type_value
| unaryExpression
| uniqueFormalParameters
| updateExpression
| valref
| value
| variableDeclaration
| variableDeclarationList
| variableStatement
| voption
| withStatement.

Inductive constructor_of_withStatement: Set :=
| WithSTMT : constructor_of_withStatement.

Inductive constructor_of_voption: Set :=
| VNone : constructor_of_voption
| VSome : constructor_of_voption.

Inductive constructor_of_variableStatement: Set :=
| VarSTMT : constructor_of_variableStatement.

Inductive constructor_of_variableDeclarationList: Set :=
| VarDeclLST : constructor_of_variableDeclarationList
| VarDeclLST_Decl : constructor_of_variableDeclarationList.

Inductive constructor_of_variableDeclaration: Set :=
| VarDecl_ID : constructor_of_variableDeclaration
| VarDecl_Pattern : constructor_of_variableDeclaration.

Inductive constructor_of_value: Set :=
| BigInt : constructor_of_value
| Boolean : constructor_of_value
| Null : constructor_of_value
| Number : constructor_of_value
| Obj : constructor_of_value
| Str : constructor_of_value
| Symbol : constructor_of_value
| Undefined : constructor_of_value.

Inductive constructor_of_valref: Set :=
| Reference : constructor_of_valref
| Value : constructor_of_valref.

Inductive constructor_of_updateExpression: Set :=
| UpdE_postDec : constructor_of_updateExpression
| UpdE_postInc : constructor_of_updateExpression
| UpdE_preDec : constructor_of_updateExpression
| UpdE_preInc : constructor_of_updateExpression
| UpdExp : constructor_of_updateExpression.

Inductive constructor_of_uniqueFormalParameters: Set :=
| UniFormPars : constructor_of_uniqueFormalParameters.

Inductive constructor_of_unaryExpression: Set :=
| UnaE_await : constructor_of_unaryExpression
| UnaE_bang : constructor_of_unaryExpression
| UnaE_delete : constructor_of_unaryExpression
| UnaE_minus : constructor_of_unaryExpression
| UnaE_plus : constructor_of_unaryExpression
| UnaE_tilde : constructor_of_unaryExpression
| UnaE_typeof : constructor_of_unaryExpression
| UnaE_void : constructor_of_unaryExpression
| UnaExp : constructor_of_unaryExpression.

Inductive constructor_of_type_value: Set :=
| T_BigInt : constructor_of_type_value
| T_Boolean : constructor_of_type_value
| T_Null : constructor_of_type_value
| T_Number : constructor_of_type_value
| T_Obj : constructor_of_type_value
| T_Str : constructor_of_type_value
| T_Symbol : constructor_of_type_value
| T_Undefined : constructor_of_type_value.

Inductive constructor_of_type_valref: Set :=
| T_Reference : constructor_of_type_valref
| T_Value : constructor_of_type_valref.

Inductive constructor_of_type_reference: Set :=
| T_R_EnvironmentRecord : constructor_of_type_reference
| T_R_Value : constructor_of_type_reference.

Inductive constructor_of_type_maybeUndefined: Set :=
| T_MU_Defined : constructor_of_type_maybeUndefined
| T_MU_Undefined : constructor_of_type_maybeUndefined.

Inductive constructor_of_type_maybeNull: Set :=
| T_MN_NotNull : constructor_of_type_maybeNull
| T_MN_Null : constructor_of_type_maybeNull.

Inductive constructor_of_type_maybeEmpty: Set :=
| T_Empty : constructor_of_type_maybeEmpty
| T_NotEmpty : constructor_of_type_maybeEmpty.

Inductive constructor_of_type_internalMethod: Set :=
| BuiltInExoticMethod : constructor_of_type_internalMethod
| BuiltInFunctionMethod : constructor_of_type_internalMethod
| FunctionMethod : constructor_of_type_internalMethod
| OrdinaryMethod : constructor_of_type_internalMethod
| ProxyObjectMethod : constructor_of_type_internalMethod.

Inductive constructor_of_type_exoticInternalMethod: Set :=
| ArgumentsMethod : constructor_of_type_exoticInternalMethod
| ArrayMethod : constructor_of_type_exoticInternalMethod
| BoundFunctionMethod : constructor_of_type_exoticInternalMethod
| ImmutablePrototypeMethod : constructor_of_type_exoticInternalMethod
| IntegerIndexedMethod : constructor_of_type_exoticInternalMethod
| ModuleNamespaceMethod : constructor_of_type_exoticInternalMethod
| StrMethod : constructor_of_type_exoticInternalMethod.

Inductive constructor_of_type_EnvironmentRecord: Set :=
| DeclarativeEnvironment : constructor_of_type_EnvironmentRecord
| GlobalEnvironment : constructor_of_type_EnvironmentRecord
| ObjectEnvironment : constructor_of_type_EnvironmentRecord.

Inductive constructor_of_type_DeclarativeEnvironmentRecord: Set :=
| Declarative : constructor_of_type_DeclarativeEnvironmentRecord
| Function : constructor_of_type_DeclarativeEnvironmentRecord
| Module : constructor_of_type_DeclarativeEnvironmentRecord.

Inductive constructor_of_throwStatement: Set :=
| ThrSTMT : constructor_of_throwStatement.

Inductive constructor_of_thisBindingStatus: Set :=
| TB_Initialized : constructor_of_thisBindingStatus
| TB_Lexical : constructor_of_thisBindingStatus
| TB_Uninitialized : constructor_of_thisBindingStatus.

Inductive constructor_of_sync: Set :=
| Async : constructor_of_sync
| Sync : constructor_of_sync.

Inductive constructor_of_superProperty: Set :=
| SP_Expression : constructor_of_superProperty
| SP_IdentifierName : constructor_of_superProperty.

Inductive constructor_of_superCall: Set :=
| SC_Arguments : constructor_of_superCall.

Inductive constructor_of_statementListItem: Set :=
| STMTListIt_Decl : constructor_of_statementListItem
| STMTListIt_STMT : constructor_of_statementListItem.

Inductive constructor_of_statementList: Set :=
| STMTList : constructor_of_statementList
| STMTList_Item : constructor_of_statementList.

Inductive constructor_of_statement: Set :=
| BlockStatement : constructor_of_statement
| BreakableStatement : constructor_of_statement
| ContinueStatement : constructor_of_statement
| DebuggerStatement : constructor_of_statement
| EmptyStatement : constructor_of_statement
| ExpressionStatement : constructor_of_statement
| IfStatement : constructor_of_statement
| LabelledStatement : constructor_of_statement
| ReturnStatement : constructor_of_statement
| ThrowStatement : constructor_of_statement
| TryStatement : constructor_of_statement
| VariableStatement : constructor_of_statement
| WithStatement : constructor_of_statement.

Inductive constructor_of_spreadElement: Set :=
| SE_AssignmentExpression : constructor_of_spreadElement.

Inductive constructor_of_singleNameBinding: Set :=
| SNB : constructor_of_singleNameBinding.

Inductive constructor_of_shortCircuitExpression: Set :=
| SCE_CoaE : constructor_of_shortCircuitExpression
| SCE_LOE : constructor_of_shortCircuitExpression.

Inductive constructor_of_shiftExpression: Set :=
| ShExp_Additive : constructor_of_shiftExpression
| ShExp_LeftShift : constructor_of_shiftExpression
| ShExp_SignRightShift : constructor_of_shiftExpression
| ShExp_UnsignRightShift : constructor_of_shiftExpression.

Inductive constructor_of_scriptBody: Set :=
| ScriptBody : constructor_of_scriptBody.

Inductive constructor_of_script: Set :=
| Script : constructor_of_script.

Inductive constructor_of_returnStatement: Set :=
| RetSTMT : constructor_of_returnStatement
| RetSTMT_ID : constructor_of_returnStatement.

Inductive constructor_of_relationalExpression: Set :=
| RelExp_Shift : constructor_of_relationalExpression
| RelExp_geq : constructor_of_relationalExpression
| RelExp_greater : constructor_of_relationalExpression
| RelExp_in : constructor_of_relationalExpression
| RelExp_instanceof : constructor_of_relationalExpression
| RelExp_leq : constructor_of_relationalExpression
| RelExp_lower : constructor_of_relationalExpression.

Inductive constructor_of_reference_bv: Set :=
| R_EnvironmentRecord : constructor_of_reference_bv
| R_Value : constructor_of_reference_bv.

Inductive constructor_of_propertyName: Set :=
| PN_ComputedPropertyName : constructor_of_propertyName
| PN_LiteralPropertyName : constructor_of_propertyName.

Inductive constructor_of_propertyDefinitionList: Set :=
| PDL_PropertyDefinition : constructor_of_propertyDefinitionList
| PDL_PropertyDefinitionList : constructor_of_propertyDefinitionList.

Inductive constructor_of_propertyDefinition: Set :=
| PD_AssignmentExpression : constructor_of_propertyDefinition
| PD_CoverInitializedName : constructor_of_propertyDefinition
| PD_IdentifierReference : constructor_of_propertyDefinition
| PD_MethodDefinition : constructor_of_propertyDefinition
| PD_PropertyNameAssignmentExpression : constructor_of_propertyDefinition.

Inductive constructor_of_primitivePreference: Set :=
| PP_Number : constructor_of_primitivePreference
| PP_Str : constructor_of_primitivePreference.

Inductive constructor_of_primaryExpression: Set :=
| PE_ArrayLiteral : constructor_of_primaryExpression
| PE_AsyncFunctionExpression : constructor_of_primaryExpression
| PE_AsyncGeneratorExpression : constructor_of_primaryExpression
| PE_ClassExpression : constructor_of_primaryExpression
| PE_CoverParenthesizedExpressionAndArrowParameterList : constructor_of_primaryExpression
| PE_FunctionExpression : constructor_of_primaryExpression
| PE_GeneratorExpression : constructor_of_primaryExpression
| PE_IdentifierReference : constructor_of_primaryExpression
| PE_Literal : constructor_of_primaryExpression
| PE_ObjectLiteral : constructor_of_primaryExpression
| PE_RegularExpressionLiteral : constructor_of_primaryExpression
| PE_TemplateLiteral : constructor_of_primaryExpression
| PE_this : constructor_of_primaryExpression.

Inductive constructor_of_pd_Properties: Set :=
| PD_Confingurable : constructor_of_pd_Properties
| PD_CustomProperty : constructor_of_pd_Properties
| PD_Enumerable : constructor_of_pd_Properties
| PD_Get : constructor_of_pd_Properties
| PD_Set : constructor_of_pd_Properties
| PD_Value : constructor_of_pd_Properties
| PD_Writable : constructor_of_pd_Properties.

Inductive constructor_of_parenthesizedExpression: Set :=
| PE_Expression : constructor_of_parenthesizedExpression.

Inductive constructor_of_out: Set :=
| Anomaly : constructor_of_out
| Success : constructor_of_out.

Inductive constructor_of_optionalExpression: Set :=
| OE_CallExpression : constructor_of_optionalExpression
| OE_MemberExpression : constructor_of_optionalExpression
| OE_OptionalExpression : constructor_of_optionalExpression.

Inductive constructor_of_optionalChain: Set :=
| OC_Arguments : constructor_of_optionalChain
| OC_Expression : constructor_of_optionalChain
| OC_IdentifierName : constructor_of_optionalChain
| OC_QArguments : constructor_of_optionalChain
| OC_QExpression : constructor_of_optionalChain
| OC_QIdentifierName : constructor_of_optionalChain
| OC_QTemplateLiteral : constructor_of_optionalChain
| OC_TemplateLiteral : constructor_of_optionalChain.

Inductive constructor_of_objectLiteral: Set :=
| OL_Empty : constructor_of_objectLiteral
| OL_PropertyDefinitionList : constructor_of_objectLiteral
| OL_PropertyDefinitionListComma : constructor_of_objectLiteral.

Inductive constructor_of_objectBindingPattern: Set :=
| OBP : constructor_of_objectBindingPattern
| OBP_Empty : constructor_of_objectBindingPattern
| OBP_PropList : constructor_of_objectBindingPattern
| OBP_Rest : constructor_of_objectBindingPattern.

Inductive constructor_of_objectAssignmentPattern: Set :=
| OAP : constructor_of_objectAssignmentPattern
| OAP_AssPropList : constructor_of_objectAssignmentPattern
| OAP_AssRestProp : constructor_of_objectAssignmentPattern
| OAP_Empty : constructor_of_objectAssignmentPattern.

Inductive constructor_of_numericLiteral: Set :=
| DecimalBigIntegerLiteral : constructor_of_numericLiteral
| DecimalLiteral : constructor_of_numericLiteral
| NonDecimalIntegerLiteral : constructor_of_numericLiteral
| NonDecimalIntegerLiteralBigIntLiteralSuffix : constructor_of_numericLiteral.

Inductive constructor_of_nullLiteral: Set :=
| NullLiteral : constructor_of_nullLiteral.

Inductive constructor_of_newTarget: Set :=
| New_Target : constructor_of_newTarget.

Inductive constructor_of_newExpression: Set :=
| NE_MemberExpression : constructor_of_newExpression
| NE_NewExpression : constructor_of_newExpression.

Inductive constructor_of_mutability: Set :=
| Immutable : constructor_of_mutability
| Mutable : constructor_of_mutability.

Inductive constructor_of_multiplicativeOperator: Set :=
| Div : constructor_of_multiplicativeOperator
| Mod : constructor_of_multiplicativeOperator
| Mul : constructor_of_multiplicativeOperator.

Inductive constructor_of_multiplicativeExpression: Set :=
| MulE_Exponentiation : constructor_of_multiplicativeExpression
| MulE_Multiplicative : constructor_of_multiplicativeExpression.

Inductive constructor_of_metaProperty: Set :=
| MP_ImportMeta : constructor_of_metaProperty
| MP_NewTarget : constructor_of_metaProperty.

Inductive constructor_of_memberExpression: Set :=
| ME_Expression : constructor_of_memberExpression
| ME_IdentifierName : constructor_of_memberExpression
| ME_MetaProperty : constructor_of_memberExpression
| ME_NewMemberExpression : constructor_of_memberExpression
| ME_PrimaryExpression : constructor_of_memberExpression
| ME_SuperProperty : constructor_of_memberExpression
| ME_TemplateLiteral : constructor_of_memberExpression.

Inductive constructor_of_maybeUndefined: Set :=
| MU_Defined : constructor_of_maybeUndefined
| MU_Undefined : constructor_of_maybeUndefined.

Inductive constructor_of_maybeNull: Set :=
| MN_NotNull : constructor_of_maybeNull
| MN_Null : constructor_of_maybeNull.

Inductive constructor_of_maybeEmpty: Set :=
| Empty : constructor_of_maybeEmpty
| NotEmpty : constructor_of_maybeEmpty.

Inductive constructor_of_logicalORExpression: Set :=
| LOE : constructor_of_logicalORExpression
| LOE_LAE : constructor_of_logicalORExpression.

Inductive constructor_of_logicalANDExpression: Set :=
| LAE : constructor_of_logicalANDExpression
| LAE_BOR : constructor_of_logicalANDExpression.

Inductive constructor_of_loc_scriptOrModule: Set :=
| LOC_ModuleRecord : constructor_of_loc_scriptOrModule
| LOC_ScriptRecord : constructor_of_loc_scriptOrModule.

Inductive constructor_of_loc_Object: Set :=
| ObjectLocation_Intrinsic : constructor_of_loc_Object
| ObjectLocation_Object : constructor_of_loc_Object.

Inductive constructor_of_literalPropertyName: Set :=
| LPN_IdentifierName : constructor_of_literalPropertyName
| LPN_NumericLiteral : constructor_of_literalPropertyName
| LPN_StrLiteral : constructor_of_literalPropertyName.

Inductive constructor_of_literal: Set :=
| Lit_BooleanLiteral : constructor_of_literal
| Lit_NullLiteral : constructor_of_literal
| Lit_NumericLiteral : constructor_of_literal
| Lit_StrLiteral : constructor_of_literal.

Inductive constructor_of_lexical_this: Set :=
| Lexical_this : constructor_of_lexical_this
| Non_lexical_this : constructor_of_lexical_this.

Inductive constructor_of_lexicalEnvironment: Set :=
| LE_Null : constructor_of_lexicalEnvironment
| LexicalEnvironment : constructor_of_lexicalEnvironment.

Inductive constructor_of_lexicalDeclaration: Set :=
| LexDecl : constructor_of_lexicalDeclaration.

Inductive constructor_of_lexicalBinding: Set :=
| LexBind_ID : constructor_of_lexicalBinding
| LexBind_Pattern : constructor_of_lexicalBinding.

Inductive constructor_of_letOrConst: Set :=
| Const : constructor_of_letOrConst
| Let_0 : constructor_of_letOrConst.

Inductive constructor_of_leftHandSideExpression: Set :=
| LHSE_CallExpression : constructor_of_leftHandSideExpression
| LHSE_NewExpression : constructor_of_leftHandSideExpression
| LHSE_OptionalExpression : constructor_of_leftHandSideExpression.

Inductive constructor_of_labelledStatement: Set :=
| LabelSTMT : constructor_of_labelledStatement.

Inductive constructor_of_labelledItem: Set :=
| LabIt_FunDec : constructor_of_labelledItem
| LabIt_STMT : constructor_of_labelledItem.

Inductive constructor_of_labelIdentifier: Set :=
| LI_await : constructor_of_labelIdentifier
| LI_identifier : constructor_of_labelIdentifier
| LI_yield : constructor_of_labelIdentifier.

Inductive constructor_of_iterationStatement: Set :=
| DoWhile : constructor_of_iterationStatement
| ForAwaitForBind : constructor_of_iterationStatement
| ForAwaitForDecl : constructor_of_iterationStatement
| ForAwaitLHS : constructor_of_iterationStatement
| ForExpr : constructor_of_iterationStatement
| ForForBindof : constructor_of_iterationStatement
| ForForDeclin : constructor_of_iterationStatement
| ForForDeclof : constructor_of_iterationStatement
| ForLHSin : constructor_of_iterationStatement
| ForLHSof : constructor_of_iterationStatement
| ForLexDecl : constructor_of_iterationStatement
| ForVarBindin : constructor_of_iterationStatement
| ForVarDecl : constructor_of_iterationStatement
| While : constructor_of_iterationStatement.

Inductive constructor_of_intrinsicObject: Set :=
| IntrinsicArray : constructor_of_intrinsicObject
| IntrinsicArrayBuffer : constructor_of_intrinsicObject
| IntrinsicArrayBufferPrototype : constructor_of_intrinsicObject
| IntrinsicArrayIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicArrayProto_entries : constructor_of_intrinsicObject
| IntrinsicArrayProto_forEach : constructor_of_intrinsicObject
| IntrinsicArrayProto_keys : constructor_of_intrinsicObject
| IntrinsicArrayProto_values : constructor_of_intrinsicObject
| IntrinsicArrayPrototype : constructor_of_intrinsicObject
| IntrinsicAsyncFromSyncIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicAsyncFunction : constructor_of_intrinsicObject
| IntrinsicAsyncFunctionPrototype : constructor_of_intrinsicObject
| IntrinsicAsyncGenerator : constructor_of_intrinsicObject
| IntrinsicAsyncGeneratorFunction : constructor_of_intrinsicObject
| IntrinsicAsyncGeneratorPrototype : constructor_of_intrinsicObject
| IntrinsicAsyncIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicAtomics : constructor_of_intrinsicObject
| IntrinsicBoolean : constructor_of_intrinsicObject
| IntrinsicBooleanPrototype : constructor_of_intrinsicObject
| IntrinsicDataView : constructor_of_intrinsicObject
| IntrinsicDataViewPrototype : constructor_of_intrinsicObject
| IntrinsicDate : constructor_of_intrinsicObject
| IntrinsicDatePrototype : constructor_of_intrinsicObject
| IntrinsicDecodeURI : constructor_of_intrinsicObject
| IntrinsicDecodeURIComponent : constructor_of_intrinsicObject
| IntrinsicEncodeURI : constructor_of_intrinsicObject
| IntrinsicEncodeURIComponent : constructor_of_intrinsicObject
| IntrinsicError : constructor_of_intrinsicObject
| IntrinsicErrorPrototype : constructor_of_intrinsicObject
| IntrinsicEval : constructor_of_intrinsicObject
| IntrinsicEvalError : constructor_of_intrinsicObject
| IntrinsicEvalErrorPrototype : constructor_of_intrinsicObject
| IntrinsicFloat32Array : constructor_of_intrinsicObject
| IntrinsicFloat32ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicFloat64Array : constructor_of_intrinsicObject
| IntrinsicFloat64ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicFunction : constructor_of_intrinsicObject
| IntrinsicFunctionPrototype : constructor_of_intrinsicObject
| IntrinsicGenerator : constructor_of_intrinsicObject
| IntrinsicGeneratorFunction : constructor_of_intrinsicObject
| IntrinsicGeneratorPrototype : constructor_of_intrinsicObject
| IntrinsicInt16Array : constructor_of_intrinsicObject
| IntrinsicInt16ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicInt32Array : constructor_of_intrinsicObject
| IntrinsicInt32ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicInt8Array : constructor_of_intrinsicObject
| IntrinsicInt8ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicIsFinite : constructor_of_intrinsicObject
| IntrinsicIsNan : constructor_of_intrinsicObject
| IntrinsicIteratorType : constructor_of_intrinsicObject
| IntrinsicJSON : constructor_of_intrinsicObject
| IntrinsicJSONParse : constructor_of_intrinsicObject
| IntrinsicJSONStrify : constructor_of_intrinsicObject
| IntrinsicMap : constructor_of_intrinsicObject
| IntrinsicMapIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicMapPrototype : constructor_of_intrinsicObject
| IntrinsicMath : constructor_of_intrinsicObject
| IntrinsicNumber : constructor_of_intrinsicObject
| IntrinsicNumberPrototype : constructor_of_intrinsicObject
| IntrinsicObjProto_toStr : constructor_of_intrinsicObject
| IntrinsicObjProto_valueOf : constructor_of_intrinsicObject
| IntrinsicObject : constructor_of_intrinsicObject
| IntrinsicObjectPrototype : constructor_of_intrinsicObject
| IntrinsicParseFloat : constructor_of_intrinsicObject
| IntrinsicParseInt : constructor_of_intrinsicObject
| IntrinsicPromise : constructor_of_intrinsicObject
| IntrinsicPromiseProto_then : constructor_of_intrinsicObject
| IntrinsicPromisePrototype : constructor_of_intrinsicObject
| IntrinsicPromise_all : constructor_of_intrinsicObject
| IntrinsicPromise_reject : constructor_of_intrinsicObject
| IntrinsicPromise_resolve : constructor_of_intrinsicObject
| IntrinsicProxy : constructor_of_intrinsicObject
| IntrinsicRangeError : constructor_of_intrinsicObject
| IntrinsicRangeErrorPrototype : constructor_of_intrinsicObject
| IntrinsicReferenceError : constructor_of_intrinsicObject
| IntrinsicReferenceErrorPrototype : constructor_of_intrinsicObject
| IntrinsicReflect : constructor_of_intrinsicObject
| IntrinsicRegExp : constructor_of_intrinsicObject
| IntrinsicRegExpPrototype : constructor_of_intrinsicObject
| IntrinsicSet : constructor_of_intrinsicObject
| IntrinsicSetIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicSetPrototype : constructor_of_intrinsicObject
| IntrinsicSharedArrayBuffer : constructor_of_intrinsicObject
| IntrinsicSharedArrayBufferPrototype : constructor_of_intrinsicObject
| IntrinsicStr : constructor_of_intrinsicObject
| IntrinsicStrIteratorPrototype : constructor_of_intrinsicObject
| IntrinsicStrPrototype : constructor_of_intrinsicObject
| IntrinsicSymbol : constructor_of_intrinsicObject
| IntrinsicSymbolPrototype : constructor_of_intrinsicObject
| IntrinsicSyntaxError : constructor_of_intrinsicObject
| IntrinsicSyntaxErrorPrototype : constructor_of_intrinsicObject
| IntrinsicThrowTypeError : constructor_of_intrinsicObject
| IntrinsicTypeError : constructor_of_intrinsicObject
| IntrinsicTypeErrorPrototype : constructor_of_intrinsicObject
| IntrinsicTypedArray : constructor_of_intrinsicObject
| IntrinsicTypedArrayPrototype : constructor_of_intrinsicObject
| IntrinsicURIError : constructor_of_intrinsicObject
| IntrinsicURIErrorPrototype : constructor_of_intrinsicObject
| IntrinsicUint16Array : constructor_of_intrinsicObject
| IntrinsicUint16ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicUint32Array : constructor_of_intrinsicObject
| IntrinsicUint32ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicUint8Array : constructor_of_intrinsicObject
| IntrinsicUint8ArrayPrototype : constructor_of_intrinsicObject
| IntrinsicUint8ClampedArray : constructor_of_intrinsicObject
| IntrinsicUint8ClampedArrayPrototype : constructor_of_intrinsicObject
| IntrinsicWeakMap : constructor_of_intrinsicObject
| IntrinsicWeakMapPrototype : constructor_of_intrinsicObject
| IntrinsicWeakSet : constructor_of_intrinsicObject
| IntrinsicWeakSetPrototype : constructor_of_intrinsicObject.

Inductive constructor_of_internalSlot: Set :=
| ConstructorKind : constructor_of_internalSlot
| ECMAScriptCode : constructor_of_internalSlot
| Environment : constructor_of_internalSlot
| Extensible : constructor_of_internalSlot
| FormalParameters : constructor_of_internalSlot
| HomeObject : constructor_of_internalSlot
| IsClassConstructor_Of_: constructor_of_internalSlot
| Prototype : constructor_of_internalSlot
| Realm : constructor_of_internalSlot
| ScriptOrModule : constructor_of_internalSlot
| SourceText : constructor_of_internalSlot
| Strict : constructor_of_internalSlot
| ThisMode : constructor_of_internalSlot.

Inductive constructor_of_integrityLevel: Set :=
| Frozen : constructor_of_integrityLevel
| Sealed : constructor_of_integrityLevel.

Inductive constructor_of_initializer: Set :=
| Init : constructor_of_initializer.

Inductive constructor_of_importMeta: Set :=
| Import_Meta : constructor_of_importMeta.

Inductive constructor_of_importCall: Set :=
| IC_AssignmentExpression : constructor_of_importCall.

Inductive constructor_of_ifStatement: Set :=
| If : constructor_of_ifStatement
| IfElse : constructor_of_ifStatement.

Inductive constructor_of_identifierReference: Set :=
| IR_await : constructor_of_identifierReference
| IR_identifier : constructor_of_identifierReference
| IR_yield : constructor_of_identifierReference.

Inductive constructor_of_identifier: Set :=
| IdentifierName : constructor_of_identifier.

Inductive constructor_of_hoistableDeclaration: Set :=
| AsyncFunctionDeclaration : constructor_of_hoistableDeclaration
| AsyncGeneratorDeclaration : constructor_of_hoistableDeclaration
| FunctionDeclaration : constructor_of_hoistableDeclaration
| GeneratorDeclaration : constructor_of_hoistableDeclaration.

Inductive constructor_of_functionStatementList: Set :=
| FuncSTMTList : constructor_of_functionStatementList.

Inductive constructor_of_functionRestParameter: Set :=
| FunRestPar : constructor_of_functionRestParameter.

Inductive constructor_of_functionMode: Set :=
| F_Global : constructor_of_functionMode
| F_Lexical : constructor_of_functionMode
| F_Strict : constructor_of_functionMode.

Inductive constructor_of_functionExpression: Set :=
| FuncExpr : constructor_of_functionExpression.

Inductive constructor_of_functionDeclaration: Set :=
| FuncDecl : constructor_of_functionDeclaration
| FuncDecl_Bound : constructor_of_functionDeclaration.

Inductive constructor_of_functionBody: Set :=
| FuncBody : constructor_of_functionBody.

Inductive constructor_of_formalParameters: Set :=
| FormPars : constructor_of_formalParameters
| FormPars_CommaList : constructor_of_formalParameters
| FormPars_Empty : constructor_of_formalParameters
| FormPars_List : constructor_of_formalParameters
| FormPars_RestParam : constructor_of_formalParameters.

Inductive constructor_of_formalParameterList: Set :=
| FormParList : constructor_of_formalParameterList
| FormParList_Par : constructor_of_formalParameterList.

Inductive constructor_of_formalParameter: Set :=
| FormPar : constructor_of_formalParameter.

Inductive constructor_of_forDeclaration: Set :=
| ForDecl : constructor_of_forDeclaration.

Inductive constructor_of_forBinding: Set :=
| ForBind_Id : constructor_of_forBinding
| ForBind_Patt : constructor_of_forBinding.

Inductive constructor_of_expressionStatement: Set :=
| ExprSTMT : constructor_of_expressionStatement.

Inductive constructor_of_expression: Set :=
| Expr_AssExpr : constructor_of_expression
| Expression : constructor_of_expression.

Inductive constructor_of_exponentiationExpression: Set :=
| EE_Exponentiation : constructor_of_exponentiationExpression
| EE_UnaryExpression : constructor_of_exponentiationExpression.

Inductive constructor_of_equalityExpression: Set :=
| EqExp_Relational : constructor_of_equalityExpression
| EqExp_eq : constructor_of_equalityExpression
| EqExp_neq : constructor_of_equalityExpression
| EqExp_strictEq : constructor_of_equalityExpression
| EqExp_strictNeq : constructor_of_equalityExpression.

Inductive constructor_of_elision: Set :=
| E_Comma : constructor_of_elision
| E_Elision : constructor_of_elision.

Inductive constructor_of_elementList: Set :=
| EL_ElementListAssignmentExpression : constructor_of_elementList
| EL_ElementListSpreadElement : constructor_of_elementList
| EL_ElisionAssignmentExpression : constructor_of_elementList
| EL_ElisionSpreadElement : constructor_of_elementList.

Inductive constructor_of_destructuringAssignmentTarget: Set :=
| DAT : constructor_of_destructuringAssignmentTarget.

Inductive constructor_of_declaration: Set :=
| ClassDeclaration : constructor_of_declaration
| HoistableDeclaration : constructor_of_declaration
| LexicalDeclaration : constructor_of_declaration.

Inductive constructor_of_coverParenthesizedExpressionAndArrowParameterList: Set :=
| CPEAAPL_BindingIdentifier : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_Expression : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionBindingIdentifier : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionBindingPattern : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_ExpressionComma : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_bindingPattern : constructor_of_coverParenthesizedExpressionAndArrowParameterList
| CPEAAPL_empty : constructor_of_coverParenthesizedExpressionAndArrowParameterList.

Inductive constructor_of_coverInitializedName: Set :=
| CIN : constructor_of_coverInitializedName.

Inductive constructor_of_coverCallExpressionAndAsyncArrowHead: Set :=
| CCEAAAH : constructor_of_coverCallExpressionAndAsyncArrowHead.

Inductive constructor_of_continueStatement: Set :=
| ContSTMT : constructor_of_continueStatement
| ContSTMT_ID : constructor_of_continueStatement.

Inductive constructor_of_constructorKind: Set :=
| CK_Base : constructor_of_constructorKind
| CK_Derived : constructor_of_constructorKind.

Inductive constructor_of_conditionalExpression: Set :=
| CondE : constructor_of_conditionalExpression
| CondE_ShortCircuit : constructor_of_conditionalExpression.

Inductive constructor_of_computedPropertyName: Set :=
| CPN : constructor_of_computedPropertyName.

Inductive constructor_of_computationFlow: Set :=
| ContinueComputation : constructor_of_computationFlow
| ReturnAbruption : constructor_of_computationFlow
| ReturnComputation : constructor_of_computationFlow.

Inductive constructor_of_completionValue: Set :=
| Abruption : constructor_of_completionValue
| Ok : constructor_of_completionValue.

Inductive constructor_of_completionType: Set :=
| Break : constructor_of_completionType
| Continue : constructor_of_completionType
| Normal : constructor_of_completionType
| Return : constructor_of_completionType
| Throw : constructor_of_completionType.

Inductive constructor_of_codeEvaluationState: Set :=
| Perform : constructor_of_codeEvaluationState
| Resume : constructor_of_codeEvaluationState
| Suspend : constructor_of_codeEvaluationState.

Inductive constructor_of_coalesceExpressionHead: Set :=
| CoaEH_BOR : constructor_of_coalesceExpressionHead
| CoaEH_CoaE : constructor_of_coalesceExpressionHead.

Inductive constructor_of_coalesceExpression: Set :=
| CoaE : constructor_of_coalesceExpression.

Inductive constructor_of_callMemberExpression: Set :=
| CME : constructor_of_callMemberExpression.

Inductive constructor_of_callExpression: Set :=
| CE_Arguments : constructor_of_callExpression
| CE_CoverCallExpressionAndAsyncArrowHead : constructor_of_callExpression
| CE_Expression : constructor_of_callExpression
| CE_IdentifierName : constructor_of_callExpression
| CE_ImportCall : constructor_of_callExpression
| CE_SuperCall : constructor_of_callExpression
| CE_TemplateLiteral : constructor_of_callExpression.

Inductive constructor_of_breakableStatement: Set :=
| IterationStatement : constructor_of_breakableStatement
| SwitchStatement : constructor_of_breakableStatement.

Inductive constructor_of_breakStatement: Set :=
| BreakSTMT : constructor_of_breakStatement
| BreakSTMT_ID : constructor_of_breakStatement.

Inductive constructor_of_booleanLiteral: Set :=
| False : constructor_of_booleanLiteral
| True : constructor_of_booleanLiteral.

Inductive constructor_of_blockStatement: Set :=
| BlockSTMT : constructor_of_blockStatement.

Inductive constructor_of_block: Set :=
| Block : constructor_of_block.

Inductive constructor_of_bitwiseXORExpression: Set :=
| BXE : constructor_of_bitwiseXORExpression
| BXE_BAE : constructor_of_bitwiseXORExpression.

Inductive constructor_of_bitwiseORExpression: Set :=
| BOE : constructor_of_bitwiseORExpression
| BOE_BXE : constructor_of_bitwiseORExpression.

Inductive constructor_of_bitwiseANDExpression: Set :=
| BAE : constructor_of_bitwiseANDExpression
| BAE_Equality : constructor_of_bitwiseANDExpression.

Inductive constructor_of_bindingStatus: Set :=
| Initialized : constructor_of_bindingStatus
| Uninitialized : constructor_of_bindingStatus.

Inductive constructor_of_bindingRestProperty: Set :=
| BRP : constructor_of_bindingRestProperty.

Inductive constructor_of_bindingRestElement: Set :=
| BRE_BID : constructor_of_bindingRestElement
| BRE_Patt : constructor_of_bindingRestElement.

Inductive constructor_of_bindingPropertyList: Set :=
| BPL : constructor_of_bindingPropertyList
| BPL_Prop : constructor_of_bindingPropertyList.

Inductive constructor_of_bindingProperty: Set :=
| BindP : constructor_of_bindingProperty
| BindP_SingleName : constructor_of_bindingProperty.

Inductive constructor_of_bindingPattern: Set :=
| BindPatt_Arr : constructor_of_bindingPattern
| BindPatt_Obj : constructor_of_bindingPattern.

Inductive constructor_of_bindingList: Set :=
| BindLST : constructor_of_bindingList
| LexBind : constructor_of_bindingList.

Inductive constructor_of_bindingIdentifier: Set :=
| BI_await : constructor_of_bindingIdentifier
| BI_identifier : constructor_of_bindingIdentifier
| BI_yield : constructor_of_bindingIdentifier.

Inductive constructor_of_bindingElisionElement: Set :=
| BEE : constructor_of_bindingElisionElement.

Inductive constructor_of_bindingElementList: Set :=
| BEL : constructor_of_bindingElementList
| BEL_ElisionElem : constructor_of_bindingElementList.

Inductive constructor_of_bindingElement: Set :=
| BindE : constructor_of_bindingElement
| BindE_SingleName : constructor_of_bindingElement.

Inductive constructor_of_assignmentRestProperty: Set :=
| ARProp : constructor_of_assignmentRestProperty.

Inductive constructor_of_assignmentRestElement: Set :=
| ARE : constructor_of_assignmentRestElement.

Inductive constructor_of_assignmentPropertyList: Set :=
| APL : constructor_of_assignmentPropertyList
| APL_AssProp : constructor_of_assignmentPropertyList.

Inductive constructor_of_assignmentProperty: Set :=
| AP_IDRef : constructor_of_assignmentProperty
| AP_PropName : constructor_of_assignmentProperty.

Inductive constructor_of_assignmentPattern: Set :=
| ArrAssPattern : constructor_of_assignmentPattern
| ObjAssPattern : constructor_of_assignmentPattern.

Inductive constructor_of_assignmentOperator: Set :=
| BANDAss : constructor_of_assignmentOperator
| BORAss : constructor_of_assignmentOperator
| BXORAss : constructor_of_assignmentOperator
| DivAss : constructor_of_assignmentOperator
| ExpAss : constructor_of_assignmentOperator
| MinusAss : constructor_of_assignmentOperator
| ModAss : constructor_of_assignmentOperator
| MulAss : constructor_of_assignmentOperator
| PlusAss : constructor_of_assignmentOperator
| SLAss : constructor_of_assignmentOperator
| SSRAss : constructor_of_assignmentOperator
| USRAss : constructor_of_assignmentOperator.

Inductive constructor_of_assignmentExpression: Set :=
| AssE_ArrowFunction : constructor_of_assignmentExpression
| AssE_Assignment : constructor_of_assignmentExpression
| AssE_AssignmentOp : constructor_of_assignmentExpression
| AssE_AsyncArrowFunction : constructor_of_assignmentExpression
| AssE_CondE : constructor_of_assignmentExpression
| AssE_YieldExpression : constructor_of_assignmentExpression.

Inductive constructor_of_assignmentElisionElement: Set :=
| AEE : constructor_of_assignmentElisionElement.

Inductive constructor_of_assignmentElementList: Set :=
| AEL : constructor_of_assignmentElementList
| AEL_AssEliEl : constructor_of_assignmentElementList.

Inductive constructor_of_assignmentElement: Set :=
| AssElem : constructor_of_assignmentElement.

Inductive constructor_of_arrayLiteral: Set :=
| AL_ElementList : constructor_of_arrayLiteral
| AL_ElementListElision : constructor_of_arrayLiteral
| AL_Elision : constructor_of_arrayLiteral.

Inductive constructor_of_arrayBindingPattern: Set :=
| ABP : constructor_of_arrayBindingPattern
| ABP_ElemLST : constructor_of_arrayBindingPattern
| ABP_Elision : constructor_of_arrayBindingPattern.

Inductive constructor_of_arrayAssignmentPattern: Set :=
| AAP : constructor_of_arrayAssignmentPattern
| AAP_AssElemList : constructor_of_arrayAssignmentPattern
| AAP_Elision : constructor_of_arrayAssignmentPattern.

Inductive constructor_of_arguments: Set :=
| Args_ArgumentList : constructor_of_arguments
| Args_ArgumentListComma : constructor_of_arguments
| Args_Empty : constructor_of_arguments.

Inductive constructor_of_argumentList: Set :=
| AL_AssignmentExpression : constructor_of_argumentList
| AL_CommaAssignmentExpression : constructor_of_argumentList
| AL_CommaDotsAssignmentExpression : constructor_of_argumentList
| AL_DotsAssignmentExpression : constructor_of_argumentList.

Inductive constructor_of_additiveExpression: Set :=
| AddE_Multiplicative : constructor_of_additiveExpression
| AddE_Sub : constructor_of_additiveExpression
| AddE_Sum : constructor_of_additiveExpression.

Inductive constructor_of_abruption: Set :=
| AnomalyAbruption : constructor_of_abruption
| NotImplemented : constructor_of_abruption
| ObjectAbruption : constructor_of_abruption.

Definition constructor(t: spec_type): Set :=
  match t with
  | abruption => constructor_of_abruption
  | additiveExpression => constructor_of_additiveExpression
  | argumentList => constructor_of_argumentList
  | arguments => constructor_of_arguments
  | arrayAssignmentPattern => constructor_of_arrayAssignmentPattern
  | arrayBindingPattern => constructor_of_arrayBindingPattern
  | arrayLiteral => constructor_of_arrayLiteral
  | assignmentElementList => constructor_of_assignmentElementList
  | assignmentElement => constructor_of_assignmentElement
  | assignmentElisionElement => constructor_of_assignmentElisionElement
  | assignmentExpression => constructor_of_assignmentExpression
  | assignmentOperator => constructor_of_assignmentOperator
  | assignmentPattern => constructor_of_assignmentPattern
  | assignmentPropertyList => constructor_of_assignmentPropertyList
  | assignmentProperty => constructor_of_assignmentProperty
  | assignmentRestElement => constructor_of_assignmentRestElement
  | assignmentRestProperty => constructor_of_assignmentRestProperty
  | bindingElementList => constructor_of_bindingElementList
  | bindingElement => constructor_of_bindingElement
  | bindingElisionElement => constructor_of_bindingElisionElement
  | bindingIdentifier => constructor_of_bindingIdentifier
  | bindingList => constructor_of_bindingList
  | bindingPattern => constructor_of_bindingPattern
  | bindingPropertyList => constructor_of_bindingPropertyList
  | bindingProperty => constructor_of_bindingProperty
  | bindingRestElement => constructor_of_bindingRestElement
  | bindingRestProperty => constructor_of_bindingRestProperty
  | bindingStatus => constructor_of_bindingStatus
  | bitwiseANDExpression => constructor_of_bitwiseANDExpression
  | bitwiseORExpression => constructor_of_bitwiseORExpression
  | bitwiseXORExpression => constructor_of_bitwiseXORExpression
  | block => constructor_of_block
  | blockStatement => constructor_of_blockStatement
  | booleanLiteral => constructor_of_booleanLiteral
  | breakableStatement => constructor_of_breakableStatement
  | breakStatement => constructor_of_breakStatement
  | callExpression => constructor_of_callExpression
  | callMemberExpression => constructor_of_callMemberExpression
  | coalesceExpressionHead => constructor_of_coalesceExpressionHead
  | coalesceExpression => constructor_of_coalesceExpression
  | codeEvaluationState => constructor_of_codeEvaluationState
  | completionType => constructor_of_completionType
  | completionValue => constructor_of_completionValue
  | computationFlow => constructor_of_computationFlow
  | computedPropertyName => constructor_of_computedPropertyName
  | conditionalExpression => constructor_of_conditionalExpression
  | constructorKind => constructor_of_constructorKind
  | continueStatement => constructor_of_continueStatement
  | coverCallExpressionAndAsyncArrowHead => constructor_of_coverCallExpressionAndAsyncArrowHead
  | coverInitializedName => constructor_of_coverInitializedName
  | coverParenthesizedExpressionAndArrowParameterList => constructor_of_coverParenthesizedExpressionAndArrowParameterList
  | declaration => constructor_of_declaration
  | destructuringAssignmentTarget => constructor_of_destructuringAssignmentTarget
  | elementList => constructor_of_elementList
  | elision => constructor_of_elision
  | equalityExpression => constructor_of_equalityExpression
  | exponentiationExpression => constructor_of_exponentiationExpression
  | expression => constructor_of_expression
  | expressionStatement => constructor_of_expressionStatement
  | forBinding => constructor_of_forBinding
  | forDeclaration => constructor_of_forDeclaration
  | formalParameterList => constructor_of_formalParameterList
  | formalParameter => constructor_of_formalParameter
  | formalParameters => constructor_of_formalParameters
  | functionBody => constructor_of_functionBody
  | functionDeclaration => constructor_of_functionDeclaration
  | functionExpression => constructor_of_functionExpression
  | functionMode => constructor_of_functionMode
  | functionRestParameter => constructor_of_functionRestParameter
  | functionStatementList => constructor_of_functionStatementList
  | hoistableDeclaration => constructor_of_hoistableDeclaration
  | identifierReference => constructor_of_identifierReference
  | identifier => constructor_of_identifier
  | ifStatement => constructor_of_ifStatement
  | importCall => constructor_of_importCall
  | importMeta => constructor_of_importMeta
  | initializer => constructor_of_initializer
  | integrityLevel => constructor_of_integrityLevel
  | internalSlot => constructor_of_internalSlot
  | intrinsicObject => constructor_of_intrinsicObject
  | iterationStatement => constructor_of_iterationStatement
  | labelIdentifier => constructor_of_labelIdentifier
  | labelledItem => constructor_of_labelledItem
  | labelledStatement => constructor_of_labelledStatement
  | leftHandSideExpression => constructor_of_leftHandSideExpression
  | letOrConst => constructor_of_letOrConst
  | lexicalBinding => constructor_of_lexicalBinding
  | lexicalDeclaration => constructor_of_lexicalDeclaration
  | lexicalEnvironment => constructor_of_lexicalEnvironment
  | lexical_this => constructor_of_lexical_this
  | literalPropertyName => constructor_of_literalPropertyName
  | literal => constructor_of_literal
  | loc_Object => constructor_of_loc_Object
  | loc_scriptOrModule => constructor_of_loc_scriptOrModule
  | logicalANDExpression => constructor_of_logicalANDExpression
  | logicalORExpression => constructor_of_logicalORExpression
  | maybeEmpty => constructor_of_maybeEmpty
  | maybeNull => constructor_of_maybeNull
  | maybeUndefined => constructor_of_maybeUndefined
  | memberExpression => constructor_of_memberExpression
  | metaProperty => constructor_of_metaProperty
  | multiplicativeExpression => constructor_of_multiplicativeExpression
  | multiplicativeOperator => constructor_of_multiplicativeOperator
  | mutability => constructor_of_mutability
  | newExpression => constructor_of_newExpression
  | newTarget => constructor_of_newTarget
  | nullLiteral => constructor_of_nullLiteral
  | numericLiteral => constructor_of_numericLiteral
  | objectAssignmentPattern => constructor_of_objectAssignmentPattern
  | objectBindingPattern => constructor_of_objectBindingPattern
  | objectLiteral => constructor_of_objectLiteral
  | optionalChain => constructor_of_optionalChain
  | optionalExpression => constructor_of_optionalExpression
  | out => constructor_of_out
  | parenthesizedExpression => constructor_of_parenthesizedExpression
  | pd_Properties => constructor_of_pd_Properties
  | primaryExpression => constructor_of_primaryExpression
  | primitivePreference => constructor_of_primitivePreference
  | propertyDefinitionList => constructor_of_propertyDefinitionList
  | propertyDefinition => constructor_of_propertyDefinition
  | propertyName => constructor_of_propertyName
  | reference_bv => constructor_of_reference_bv
  | relationalExpression => constructor_of_relationalExpression
  | returnStatement => constructor_of_returnStatement
  | scriptBody => constructor_of_scriptBody
  | script => constructor_of_script
  | shiftExpression => constructor_of_shiftExpression
  | shortCircuitExpression => constructor_of_shortCircuitExpression
  | singleNameBinding => constructor_of_singleNameBinding
  | spreadElement => constructor_of_spreadElement
  | statementListItem => constructor_of_statementListItem
  | statementList => constructor_of_statementList
  | statement => constructor_of_statement
  | superCall => constructor_of_superCall
  | superProperty => constructor_of_superProperty
  | sync => constructor_of_sync
  | thisBindingStatus => constructor_of_thisBindingStatus
  | throwStatement => constructor_of_throwStatement
  | type_DeclarativeEnvironmentRecord => constructor_of_type_DeclarativeEnvironmentRecord
  | type_EnvironmentRecord => constructor_of_type_EnvironmentRecord
  | type_exoticInternalMethod => constructor_of_type_exoticInternalMethod
  | type_internalMethod => constructor_of_type_internalMethod
  | type_maybeEmpty => constructor_of_type_maybeEmpty
  | type_maybeNull => constructor_of_type_maybeNull
  | type_maybeUndefined => constructor_of_type_maybeUndefined
  | type_reference => constructor_of_type_reference
  | type_valref => constructor_of_type_valref
  | type_value => constructor_of_type_value
  | unaryExpression => constructor_of_unaryExpression
  | uniqueFormalParameters => constructor_of_uniqueFormalParameters
  | updateExpression => constructor_of_updateExpression
  | valref => constructor_of_valref
  | value => constructor_of_value
  | variableDeclarationList => constructor_of_variableDeclarationList
  | variableDeclaration => constructor_of_variableDeclaration
  | variableStatement => constructor_of_variableStatement
  | voption => constructor_of_voption
  | withStatement => constructor_of_withStatement
  end.

Scheme Equality for constructor_of_withStatement.
Scheme Equality for constructor_of_voption.
Scheme Equality for constructor_of_variableStatement.
Scheme Equality for constructor_of_variableDeclarationList.
Scheme Equality for constructor_of_variableDeclaration.
Scheme Equality for constructor_of_value.
Scheme Equality for constructor_of_valref.
Scheme Equality for constructor_of_updateExpression.
Scheme Equality for constructor_of_uniqueFormalParameters.
Scheme Equality for constructor_of_unaryExpression.
Scheme Equality for constructor_of_type_value.
Scheme Equality for constructor_of_type_valref.
Scheme Equality for constructor_of_type_reference.
Scheme Equality for constructor_of_type_maybeUndefined.
Scheme Equality for constructor_of_type_maybeNull.
Scheme Equality for constructor_of_type_maybeEmpty.
Scheme Equality for constructor_of_type_internalMethod.
Scheme Equality for constructor_of_type_exoticInternalMethod.
Scheme Equality for constructor_of_type_EnvironmentRecord.
Scheme Equality for constructor_of_type_DeclarativeEnvironmentRecord.
Scheme Equality for constructor_of_throwStatement.
Scheme Equality for constructor_of_thisBindingStatus.
Scheme Equality for constructor_of_sync.
Scheme Equality for constructor_of_superProperty.
Scheme Equality for constructor_of_superCall.
Scheme Equality for constructor_of_statementListItem.
Scheme Equality for constructor_of_statementList.
Scheme Equality for constructor_of_statement.
Scheme Equality for constructor_of_spreadElement.
Scheme Equality for constructor_of_singleNameBinding.
Scheme Equality for constructor_of_shortCircuitExpression.
Scheme Equality for constructor_of_shiftExpression.
Scheme Equality for constructor_of_scriptBody.
Scheme Equality for constructor_of_script.
Scheme Equality for constructor_of_returnStatement.
Scheme Equality for constructor_of_relationalExpression.
Scheme Equality for constructor_of_reference_bv.
Scheme Equality for constructor_of_propertyName.
Scheme Equality for constructor_of_propertyDefinitionList.
Scheme Equality for constructor_of_propertyDefinition.
Scheme Equality for constructor_of_primitivePreference.
Scheme Equality for constructor_of_primaryExpression.
Scheme Equality for constructor_of_pd_Properties.
Scheme Equality for constructor_of_parenthesizedExpression.
Scheme Equality for constructor_of_out.
Scheme Equality for constructor_of_optionalExpression.
Scheme Equality for constructor_of_optionalChain.
Scheme Equality for constructor_of_objectLiteral.
Scheme Equality for constructor_of_objectBindingPattern.
Scheme Equality for constructor_of_objectAssignmentPattern.
Scheme Equality for constructor_of_numericLiteral.
Scheme Equality for constructor_of_nullLiteral.
Scheme Equality for constructor_of_newTarget.
Scheme Equality for constructor_of_newExpression.
Scheme Equality for constructor_of_mutability.
Scheme Equality for constructor_of_multiplicativeOperator.
Scheme Equality for constructor_of_multiplicativeExpression.
Scheme Equality for constructor_of_metaProperty.
Scheme Equality for constructor_of_memberExpression.
Scheme Equality for constructor_of_maybeUndefined.
Scheme Equality for constructor_of_maybeNull.
Scheme Equality for constructor_of_maybeEmpty.
Scheme Equality for constructor_of_logicalORExpression.
Scheme Equality for constructor_of_logicalANDExpression.
Scheme Equality for constructor_of_loc_scriptOrModule.
Scheme Equality for constructor_of_loc_Object.
Scheme Equality for constructor_of_literalPropertyName.
Scheme Equality for constructor_of_literal.
Scheme Equality for constructor_of_lexical_this.
Scheme Equality for constructor_of_lexicalEnvironment.
Scheme Equality for constructor_of_lexicalDeclaration.
Scheme Equality for constructor_of_lexicalBinding.
Scheme Equality for constructor_of_letOrConst.
Scheme Equality for constructor_of_leftHandSideExpression.
Scheme Equality for constructor_of_labelledStatement.
Scheme Equality for constructor_of_labelledItem.
Scheme Equality for constructor_of_labelIdentifier.
Scheme Equality for constructor_of_iterationStatement.

Goal 1 = 2. idtac "This one is going to be slow (~15s)". Abort.
Time Scheme Equality for constructor_of_intrinsicObject.

Scheme Equality for constructor_of_internalSlot.
Scheme Equality for constructor_of_integrityLevel.
Scheme Equality for constructor_of_initializer.
Scheme Equality for constructor_of_importMeta.
Scheme Equality for constructor_of_importCall.
Scheme Equality for constructor_of_ifStatement.
Scheme Equality for constructor_of_identifierReference.
Scheme Equality for constructor_of_identifier.
Scheme Equality for constructor_of_hoistableDeclaration.
Scheme Equality for constructor_of_functionStatementList.
Scheme Equality for constructor_of_functionRestParameter.
Scheme Equality for constructor_of_functionMode.
Scheme Equality for constructor_of_functionExpression.
Scheme Equality for constructor_of_functionDeclaration.
Scheme Equality for constructor_of_functionBody.
Scheme Equality for constructor_of_formalParameters.
Scheme Equality for constructor_of_formalParameterList.
Scheme Equality for constructor_of_formalParameter.
Scheme Equality for constructor_of_forDeclaration.
Scheme Equality for constructor_of_forBinding.
Scheme Equality for constructor_of_expressionStatement.
Scheme Equality for constructor_of_expression.
Scheme Equality for constructor_of_exponentiationExpression.
Scheme Equality for constructor_of_equalityExpression.
Scheme Equality for constructor_of_elision.
Scheme Equality for constructor_of_elementList.
Scheme Equality for constructor_of_destructuringAssignmentTarget.
Scheme Equality for constructor_of_declaration.
Scheme Equality for constructor_of_coverParenthesizedExpressionAndArrowParameterList.
Scheme Equality for constructor_of_coverInitializedName.
Scheme Equality for constructor_of_coverCallExpressionAndAsyncArrowHead.
Scheme Equality for constructor_of_continueStatement.
Scheme Equality for constructor_of_constructorKind.
Scheme Equality for constructor_of_conditionalExpression.
Scheme Equality for constructor_of_computedPropertyName.
Scheme Equality for constructor_of_computationFlow.
Scheme Equality for constructor_of_completionValue.
Scheme Equality for constructor_of_completionType.
Scheme Equality for constructor_of_codeEvaluationState.
Scheme Equality for constructor_of_coalesceExpressionHead.
Scheme Equality for constructor_of_coalesceExpression.
Scheme Equality for constructor_of_callMemberExpression.
Scheme Equality for constructor_of_callExpression.
Scheme Equality for constructor_of_breakableStatement.
Scheme Equality for constructor_of_breakStatement.
Scheme Equality for constructor_of_booleanLiteral.
Scheme Equality for constructor_of_blockStatement.
Scheme Equality for constructor_of_block.
Scheme Equality for constructor_of_bitwiseXORExpression.
Scheme Equality for constructor_of_bitwiseORExpression.
Scheme Equality for constructor_of_bitwiseANDExpression.
Scheme Equality for constructor_of_bindingStatus.
Scheme Equality for constructor_of_bindingRestProperty.
Scheme Equality for constructor_of_bindingRestElement.
Scheme Equality for constructor_of_bindingPropertyList.
Scheme Equality for constructor_of_bindingProperty.
Scheme Equality for constructor_of_bindingPattern.
Scheme Equality for constructor_of_bindingList.
Scheme Equality for constructor_of_bindingIdentifier.
Scheme Equality for constructor_of_bindingElisionElement.
Scheme Equality for constructor_of_bindingElementList.
Scheme Equality for constructor_of_bindingElement.
Scheme Equality for constructor_of_assignmentRestProperty.
Scheme Equality for constructor_of_assignmentRestElement.
Scheme Equality for constructor_of_assignmentPropertyList.
Scheme Equality for constructor_of_assignmentProperty.
Scheme Equality for constructor_of_assignmentPattern.
Scheme Equality for constructor_of_assignmentOperator.
Scheme Equality for constructor_of_assignmentExpression.
Scheme Equality for constructor_of_assignmentElisionElement.
Scheme Equality for constructor_of_assignmentElementList.
Scheme Equality for constructor_of_assignmentElement.
Scheme Equality for constructor_of_arrayLiteral.
Scheme Equality for constructor_of_arrayBindingPattern.
Scheme Equality for constructor_of_arrayAssignmentPattern.
Scheme Equality for constructor_of_arguments.
Scheme Equality for constructor_of_argumentList.
Scheme Equality for constructor_of_additiveExpression.
Scheme Equality for constructor_of_abruption.

Definition constructor_eq_dec(t: spec_type): eq_dec (constructor t) :=
  match t with
  | abruption => constructor_of_abruption_eq_dec
  | additiveExpression => constructor_of_additiveExpression_eq_dec
  | argumentList => constructor_of_argumentList_eq_dec
  | arguments => constructor_of_arguments_eq_dec
  | arrayAssignmentPattern => constructor_of_arrayAssignmentPattern_eq_dec
  | arrayBindingPattern => constructor_of_arrayBindingPattern_eq_dec
  | arrayLiteral => constructor_of_arrayLiteral_eq_dec
  | assignmentElementList => constructor_of_assignmentElementList_eq_dec
  | assignmentElement => constructor_of_assignmentElement_eq_dec
  | assignmentElisionElement => constructor_of_assignmentElisionElement_eq_dec
  | assignmentExpression => constructor_of_assignmentExpression_eq_dec
  | assignmentOperator => constructor_of_assignmentOperator_eq_dec
  | assignmentPattern => constructor_of_assignmentPattern_eq_dec
  | assignmentPropertyList => constructor_of_assignmentPropertyList_eq_dec
  | assignmentProperty => constructor_of_assignmentProperty_eq_dec
  | assignmentRestElement => constructor_of_assignmentRestElement_eq_dec
  | assignmentRestProperty => constructor_of_assignmentRestProperty_eq_dec
  | bindingElementList => constructor_of_bindingElementList_eq_dec
  | bindingElement => constructor_of_bindingElement_eq_dec
  | bindingElisionElement => constructor_of_bindingElisionElement_eq_dec
  | bindingIdentifier => constructor_of_bindingIdentifier_eq_dec
  | bindingList => constructor_of_bindingList_eq_dec
  | bindingPattern => constructor_of_bindingPattern_eq_dec
  | bindingPropertyList => constructor_of_bindingPropertyList_eq_dec
  | bindingProperty => constructor_of_bindingProperty_eq_dec
  | bindingRestElement => constructor_of_bindingRestElement_eq_dec
  | bindingRestProperty => constructor_of_bindingRestProperty_eq_dec
  | bindingStatus => constructor_of_bindingStatus_eq_dec
  | bitwiseANDExpression => constructor_of_bitwiseANDExpression_eq_dec
  | bitwiseORExpression => constructor_of_bitwiseORExpression_eq_dec
  | bitwiseXORExpression => constructor_of_bitwiseXORExpression_eq_dec
  | block => constructor_of_block_eq_dec
  | blockStatement => constructor_of_blockStatement_eq_dec
  | booleanLiteral => constructor_of_booleanLiteral_eq_dec
  | breakableStatement => constructor_of_breakableStatement_eq_dec
  | breakStatement => constructor_of_breakStatement_eq_dec
  | callExpression => constructor_of_callExpression_eq_dec
  | callMemberExpression => constructor_of_callMemberExpression_eq_dec
  | coalesceExpressionHead => constructor_of_coalesceExpressionHead_eq_dec
  | coalesceExpression => constructor_of_coalesceExpression_eq_dec
  | codeEvaluationState => constructor_of_codeEvaluationState_eq_dec
  | completionType => constructor_of_completionType_eq_dec
  | completionValue => constructor_of_completionValue_eq_dec
  | computationFlow => constructor_of_computationFlow_eq_dec
  | computedPropertyName => constructor_of_computedPropertyName_eq_dec
  | conditionalExpression => constructor_of_conditionalExpression_eq_dec
  | constructorKind => constructor_of_constructorKind_eq_dec
  | continueStatement => constructor_of_continueStatement_eq_dec
  | coverCallExpressionAndAsyncArrowHead => constructor_of_coverCallExpressionAndAsyncArrowHead_eq_dec
  | coverInitializedName => constructor_of_coverInitializedName_eq_dec
  | coverParenthesizedExpressionAndArrowParameterList => constructor_of_coverParenthesizedExpressionAndArrowParameterList_eq_dec
  | declaration => constructor_of_declaration_eq_dec
  | destructuringAssignmentTarget => constructor_of_destructuringAssignmentTarget_eq_dec
  | elementList => constructor_of_elementList_eq_dec
  | elision => constructor_of_elision_eq_dec
  | equalityExpression => constructor_of_equalityExpression_eq_dec
  | exponentiationExpression => constructor_of_exponentiationExpression_eq_dec
  | expression => constructor_of_expression_eq_dec
  | expressionStatement => constructor_of_expressionStatement_eq_dec
  | forBinding => constructor_of_forBinding_eq_dec
  | forDeclaration => constructor_of_forDeclaration_eq_dec
  | formalParameterList => constructor_of_formalParameterList_eq_dec
  | formalParameter => constructor_of_formalParameter_eq_dec
  | formalParameters => constructor_of_formalParameters_eq_dec
  | functionBody => constructor_of_functionBody_eq_dec
  | functionDeclaration => constructor_of_functionDeclaration_eq_dec
  | functionExpression => constructor_of_functionExpression_eq_dec
  | functionMode => constructor_of_functionMode_eq_dec
  | functionRestParameter => constructor_of_functionRestParameter_eq_dec
  | functionStatementList => constructor_of_functionStatementList_eq_dec
  | hoistableDeclaration => constructor_of_hoistableDeclaration_eq_dec
  | identifierReference => constructor_of_identifierReference_eq_dec
  | identifier => constructor_of_identifier_eq_dec
  | ifStatement => constructor_of_ifStatement_eq_dec
  | importCall => constructor_of_importCall_eq_dec
  | importMeta => constructor_of_importMeta_eq_dec
  | initializer => constructor_of_initializer_eq_dec
  | integrityLevel => constructor_of_integrityLevel_eq_dec
  | internalSlot => constructor_of_internalSlot_eq_dec
  | intrinsicObject => constructor_of_intrinsicObject_eq_dec
  | iterationStatement => constructor_of_iterationStatement_eq_dec
  | labelIdentifier => constructor_of_labelIdentifier_eq_dec
  | labelledItem => constructor_of_labelledItem_eq_dec
  | labelledStatement => constructor_of_labelledStatement_eq_dec
  | leftHandSideExpression => constructor_of_leftHandSideExpression_eq_dec
  | letOrConst => constructor_of_letOrConst_eq_dec
  | lexicalBinding => constructor_of_lexicalBinding_eq_dec
  | lexicalDeclaration => constructor_of_lexicalDeclaration_eq_dec
  | lexicalEnvironment => constructor_of_lexicalEnvironment_eq_dec
  | lexical_this => constructor_of_lexical_this_eq_dec
  | literalPropertyName => constructor_of_literalPropertyName_eq_dec
  | literal => constructor_of_literal_eq_dec
  | loc_Object => constructor_of_loc_Object_eq_dec
  | loc_scriptOrModule => constructor_of_loc_scriptOrModule_eq_dec
  | logicalANDExpression => constructor_of_logicalANDExpression_eq_dec
  | logicalORExpression => constructor_of_logicalORExpression_eq_dec
  | maybeEmpty => constructor_of_maybeEmpty_eq_dec
  | maybeNull => constructor_of_maybeNull_eq_dec
  | maybeUndefined => constructor_of_maybeUndefined_eq_dec
  | memberExpression => constructor_of_memberExpression_eq_dec
  | metaProperty => constructor_of_metaProperty_eq_dec
  | multiplicativeExpression => constructor_of_multiplicativeExpression_eq_dec
  | multiplicativeOperator => constructor_of_multiplicativeOperator_eq_dec
  | mutability => constructor_of_mutability_eq_dec
  | newExpression => constructor_of_newExpression_eq_dec
  | newTarget => constructor_of_newTarget_eq_dec
  | nullLiteral => constructor_of_nullLiteral_eq_dec
  | numericLiteral => constructor_of_numericLiteral_eq_dec
  | objectAssignmentPattern => constructor_of_objectAssignmentPattern_eq_dec
  | objectBindingPattern => constructor_of_objectBindingPattern_eq_dec
  | objectLiteral => constructor_of_objectLiteral_eq_dec
  | optionalChain => constructor_of_optionalChain_eq_dec
  | optionalExpression => constructor_of_optionalExpression_eq_dec
  | out => constructor_of_out_eq_dec
  | parenthesizedExpression => constructor_of_parenthesizedExpression_eq_dec
  | pd_Properties => constructor_of_pd_Properties_eq_dec
  | primaryExpression => constructor_of_primaryExpression_eq_dec
  | primitivePreference => constructor_of_primitivePreference_eq_dec
  | propertyDefinitionList => constructor_of_propertyDefinitionList_eq_dec
  | propertyDefinition => constructor_of_propertyDefinition_eq_dec
  | propertyName => constructor_of_propertyName_eq_dec
  | reference_bv => constructor_of_reference_bv_eq_dec
  | relationalExpression => constructor_of_relationalExpression_eq_dec
  | returnStatement => constructor_of_returnStatement_eq_dec
  | scriptBody => constructor_of_scriptBody_eq_dec
  | script => constructor_of_script_eq_dec
  | shiftExpression => constructor_of_shiftExpression_eq_dec
  | shortCircuitExpression => constructor_of_shortCircuitExpression_eq_dec
  | singleNameBinding => constructor_of_singleNameBinding_eq_dec
  | spreadElement => constructor_of_spreadElement_eq_dec
  | statementListItem => constructor_of_statementListItem_eq_dec
  | statementList => constructor_of_statementList_eq_dec
  | statement => constructor_of_statement_eq_dec
  | superCall => constructor_of_superCall_eq_dec
  | superProperty => constructor_of_superProperty_eq_dec
  | sync => constructor_of_sync_eq_dec
  | thisBindingStatus => constructor_of_thisBindingStatus_eq_dec
  | throwStatement => constructor_of_throwStatement_eq_dec
  | type_DeclarativeEnvironmentRecord => constructor_of_type_DeclarativeEnvironmentRecord_eq_dec
  | type_EnvironmentRecord => constructor_of_type_EnvironmentRecord_eq_dec
  | type_exoticInternalMethod => constructor_of_type_exoticInternalMethod_eq_dec
  | type_internalMethod => constructor_of_type_internalMethod_eq_dec
  | type_maybeEmpty => constructor_of_type_maybeEmpty_eq_dec
  | type_maybeNull => constructor_of_type_maybeNull_eq_dec
  | type_maybeUndefined => constructor_of_type_maybeUndefined_eq_dec
  | type_reference => constructor_of_type_reference_eq_dec
  | type_valref => constructor_of_type_valref_eq_dec
  | type_value => constructor_of_type_value_eq_dec
  | unaryExpression => constructor_of_unaryExpression_eq_dec
  | uniqueFormalParameters => constructor_of_uniqueFormalParameters_eq_dec
  | updateExpression => constructor_of_updateExpression_eq_dec
  | valref => constructor_of_valref_eq_dec
  | value => constructor_of_value_eq_dec
  | variableDeclarationList => constructor_of_variableDeclarationList_eq_dec
  | variableDeclaration => constructor_of_variableDeclaration_eq_dec
  | variableStatement => constructor_of_variableStatement_eq_dec
  | voption => constructor_of_voption_eq_dec
  | withStatement => constructor_of_withStatement_eq_dec
  end.

Eval cbv in match constructor_eq_dec abruption AnomalyAbruption NotImplemented with
            | left _ => 1
            | right _ => 0
            end.

Eval cbv in match constructor_eq_dec abruption AnomalyAbruption AnomalyAbruption with
            | left _ => 1
            | right _ => 0
            end.