Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
| NLevelLanguage_zero : forall lang, NLevelLanguage O lang
| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,
Inductive NLevelLanguage : nat -> ProgrammingLanguageSMME -> Type :=
| NLevelLanguage_zero : forall lang, NLevelLanguage O lang
| NLevelLanguage_succ : forall (L1 L2:ProgrammingLanguageSMME) n,