Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
BVNot()
BitVecN
BitVecNConst()
BitVecNVal()
BitVecSort()
PopCount()
SelectConcat()
StoreConcat()
UnConcat()
fromBV()
popcount()
popcounts()
select_concat()
select_concats()
store_concat()
store_concats()
toBV()
vmap()
x (BitVecRef)