(2steps)
PrintForm
Definitions
formula
Sections
ClassicalProps(jlc)
Doc
At:
subformula
wf
F:Formula. subformula(F)
Formula List
By:
Unfold `subformula` 0
Generated subgoal:
1
1.
F:
Formula
case F:
x
nil;
p
[p];p
q
[p; q];p
q
[p; q];p
q
[p; q];
Formula List
About:
(2steps)
PrintForm
Definitions
formula
Sections
ClassicalProps(jlc)
Doc
case F:
x
nil;
p [p];p
q [p; q];p
q [p; q];p
q [p; q]; 
Formula List
F:Formula. subformula(F) Formula List
case F:x nil;p [p];pq [p; q];pq [p; q];pq [p; q]; Formula List
