PrintForm
Definitions
elimination
Sections
ClassicalProps(jlc)
Doc
At:
formula
not
right
sat
2
1
2
2
1
1.
hyp:
Formula List
2.
M:
Formula List
3.
N:
Formula List
4.
f:
Formula
5.
a:
Assignment
6.
a |=
f
a |
f
F
hyp.a |
F
F
M.a |= F
F
N.a |= F
By:
Choose [1;1]
Generated subgoal:
1
a |
f
About:
f 
a |
f 
F
hyp.a | F FM.a |= F FN.a |= F a | f
