Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
skolem()
Defn
Judgement
LemmaError
SchemaVar()
compose()
consider()
define_fix()
defns
einstan()
forget()
forget2()
fresh_const()
generalize()
herb()
induct_inductive()
instan()
instan2()
is_defined()
is_proof()
is_schema_var()
modus()
substitute_schema_vars()
Skolemize an existential quantifier.
pf (Proof)
tuple[list[ExprRef], Proof]