concrete MathTextEng of MathText = LogicEng ** MathTextI with
  (LexLogic = LexLogicEng),
  (Syntax = SyntaxEng),
  (Lang = LangEng), ---- ImpP3
  (Symbolic = SymbolicEng) ;