Calc
FreshVar()
FreshVars()
Inductive()
Lemma()
NewType()
PTheorem()
Proof
QExists()
QForAll()
QImplies()
Struct()
Theorem()
axiom()
cond()
define()
prove()
search()
simp()
MImplies()
Box()
In()
Next()
PAnd()
PBoolRef
PDistinct()
PEq()
PExprRef
PIf()
PImplies()
POr()
PointEq()
PointIf()
Valid()
coerce()
https://en.wikipedia.org/wiki/Modal_companion
p (PBoolRef)
q (PBoolRef)