concrete MathTextFre of MathText = LogicFre ** MathTextI with
  (LexLogic = LexLogicFre),
  (Syntax = SyntaxFre),
  (Lang = LangFre), ---- ImpP3
  (Symbolic = SymbolicFre) ;