Encode  =  STT +

consts
  o     :: "term"
  imp   :: "term"
  
rules
  imp_def    "G|- imp: o->o->o"
end