PrintForm
Definitions
sat
lemmas
Sections
ClassicalProps(jlc)
Doc
At:
formula
imp
sat
lemma
1
2
2
1
1
1.
a:
Assignment
2.
q:
Formula
3.
r:
Formula
4.
(r under a) = 3
(q under a)
(r under a) = 3
By:
GenConcl ((q under a) = x)
Generated subgoal:
1
5.
x:
6.
(q under a) = x
x
(r under a) = 3
About:
x 
(r under a) = 3
(q under a) (r under a) = 3 x (r under a) = 3