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