Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
axiom_sig()
DeclareFunction()
Fin()
HasType()
Id()
Pi()
Program()
ProgramState
SubSort
TExists()
TForAll()
Telescope
Type
ann()
has_type()
normalize()
open_binder()
prove_sig()
subsort_domain()
Assign signature to a function f with a telescope of arguments tele0 as an axiom
f (FuncDeclRef)
tele0 (Telescope)
T (SubSort)