concrete PredicationFin of Predication = CatFin ** PredicationI with
  (Syntax = SyntaxFin),
  (Lang = LangFin) ;