Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
test()
>>> term_parser.parse("f(Xy1,g(y23))") Tree('fun_app', [Token('NAME', 'f'), Tree('var', [Token('UPPER_WORD', 'Xy1')]), Tree('fun_app', [Token('NAME', 'g'), Tree('const', [Token('NAME', 'y23')])])])