Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
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()
Prove that the empty set is finite for sets of T.
T (SortRef)