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()
Set difference. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const(“A”, IntSet) >>> kd.prove(diff(A, A) == IntSet.empty) |= setminus(A, A) == K(Int, False)
A (ArrayRef)
B (ArrayRef)
ArrayRef