| "qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
| "elim" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "apply" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "intros" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "assume" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "the" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "qed" { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
| "elim" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "apply" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "intros" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "assume" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }
| "the" { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s }