+ (*
+ Definition OmegaLevelLanguage : Type :=
+ { f : nat -> ProgrammingLanguage
+ & forall n, TwoLevelLanguage (f n) (f (S n)) }.
+ *)
+
+End ProgrammingLanguageReification.
+
+(*
+ Structure ProgrammingLanguage :=
+ { plsmme_t : Type
+ ; plsmme_judg : Type
+ ; plsmme_sequent : Tree ??plsmme_t -> Tree ??plsmme_t -> plsmme_judg
+ ; plsmme_rule : Tree ??plsmme_judg -> Tree ??plsmme_judg -> Type
+ ; plsmme_pl : @ProgrammingLanguage plsmme_t plsmme_judg plsmme_sequent plsmme_rule
+ ; plsmme_smme : SurjectiveEnrichment (TypesEnrichedInJudgments _ _ plsmme_pl)
+ }.
+ Coercion plsmme_pl : ProgrammingLanguage >-> ProgrammingLanguage.
+ Coercion plsmme_smme : ProgrammingLanguage >-> SurjectiveMonicMonoidalEnrichment.
+*)