Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Struct()
axiom()
cond()
define()
prove()
search()
simp()
unify()
all_values()
alpha_eq()
antipattern()
ast_size_sexpr()
decls()
free_vars()
generate()
is_subterm()
is_value()
lemma_db()
occurs()
open_binder()
open_binder_unhygienic()
pmatch()
pmatch_fo()
pmatch_rec()
prompt()
prune()
quant_kind_eq()
sanity_check_consistency()
search_decl()
search_expr()
sorts()
subterms()
unify_db()
Unification
vs (list[ExprRef])
p1 (ExprRef)
p2 (ExprRef)
dict[ExprRef, ExprRef] | None