Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
instan()
Defn
Judgement
LemmaError
andI()
compose()
define_fix()
defns
ext()
forget()
fresh_const()
generalize()
herb()
induct_inductive()
is_defined()
is_fresh_var()
is_proof()
modus()
obtain()
rename_vars2()
specialize()
subst()
unfold()
Instantiate a universally quantified formula. This is forall elimination
ts (Sequence[ExprRef])
pf (Proof)