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