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()
Complement of a set. >>> IntSet = Set(smt.IntSort()) >>> A = smt.Const(“A”, IntSet) >>> kd.prove(complement(complement(A)) == A) |= complement(complement(A)) == A
A (ArrayRef)
ArrayRef