[morpher]

It looks like -> on a line of its own means "everything before this implies everything after it". So, for your second example you want

  x,Hx->Mx
  ->
  Hs->Ms

which returns "The statement is necessarily true."