わからん、==> の使い方
NGと書いてあるところだけダメ。
(* on top of Pure *) axiomatization A:: "'a ⇒ prop" and B:: "'a ⇒ prop" and P :: "prop" and Q :: "prop" term "op ==> P Q" term "P ==> Q" (* NG *) term "(A a)" term "(B b)" term "op ==> (A a) (B b)" term "(A a) ==> (B b)" (* NG *)