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