is mentioned by

Thm* F:Formula. subformula(F) Formula List	[subformula_wf]
Thm* p,q:Formula. pq Formula	[fimp_wf]
Thm* p,q:Formula. pq Formula	[f_or_wf]
Thm* p,q:Formula. pq Formula	[fand_wf]
Thm* x:Formula. x Formula	[fnot_wf]
Thm* x:Var. x Formula	[fvar_wf]

In prior sections: core fun 1 well fnd int 1 bool 1 union rel 1 quot 1 sqequal 1 prog 1 int 2 list 1 lambda jlc bool 2 jlc discrete jlc core 3 jlc list 3 jlc var jlc

Try larger context: ClassicalProps(jlc)