Calc
Inductive()
Lemma
NewType()
Proof
QExists()
QForAll()
Record()
axiom()
cond()
define()
lemma()
instan2()
Defn
LemmaError
beta_conv()
consider()
define_fix()
defns
einstan()
forget()
forget2()
fresh_const()
herb()
instan()
is_proof()
skolem()
Instantiate a universally quantified formula forall xs, P(xs) -> P(ts) This is forall elimination