e はルール（証明の名前＝定理の名前〉、利用側からはルール。Prover's English ＝ P-En
OBTAIN ::= prove | show | present | reach | obtain
RESULT ::= conclusion | target | result
assume文 ::= {we}? assume x : X
have文 ::= {we}? have x : X {from e}
suffices文 ::= {it}? suffices {to OBTAIN} x : X because {the RESULT comes} from e
try文 ::= {so | next}? {we}? {try | proceed} {to OBTAIN}? x {: X}?
終了文 ::= {we}? OBTAINed x : X {from e}
use文 ::= {{we}? use | using} e翻訳：
assume x : X ～⇒ fun (x: X) => have x : X from e ～⇒ let x : X := e suffices x : X because from e ～⇒ suffices x : X from e try x : X ～⇒ (無し) showed x : X from e ～⇒ show x : X from e use e ～⇒ let _this_k := e
