Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
fresh_const()
Defn
Judgement
LemmaError
andI()
compose()
define_fix()
defns
ext()
forget()
generalize()
herb()
induct_inductive()
instan()
is_defined()
is_fresh_var()
is_proof()
modus()
obtain()
rename_vars2()
specialize()
subst()
unfold()
Generate fresh constants of same sort as quantifier.
q (QuantifierRef)
list[ExprRef]