PrintForm
Definitions
formula
list
Sections
ClassicalProps(jlc)
Doc
At:
list
rank
append
homomorphism
1
2
1
1
1
1.
M:
Formula List
2.
u:
Formula
3.
v:
Formula List
4.
N:
Formula List
5.
(v @ N) =
(v)+
(N)
(u)+
(v @ N) =
(u)+
(v)+
(N)
By:
HypSubst -1 0
Generated subgoals:
1
(u)+
(v)+
(N) =
(u)+
(v)+
(N)
2
6.
z:
(u)+z =
(u)+
(v)+
(N)
Prop
About:
(u)+(v)+(N) = (u)+(v)+(N) 
(u)+z = (u)+(v)+(N) Prop(v @ N) = (v)+(N) (u)+(v @ N) = (u)+(v)+(N) (u)+(v)+(N) = (u)+(v)+(N) (u)+z = (u)+(v)+(N) Prop
