Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
BigUnion()
Choose()
CountInter()
EClass()
FamilyUnion()
Finite()
Injective()
PowerSet()
Quot()
Range()
Set()
Singleton()
Surjective()
bigunion()
complement()
diff()
inter()
is_set()
member()
subset()
union()
Abstracted bigunion
T (SortRef)
FuncDeclRef