formula
list
Sections
ClassicalProps(jlc)
Doc
Def
(L) == reduce(
x,y.
(x)+y;0;L)
Thm*
M,N:Formula List.
(M @ N) =
(M)+
(N)
list_rank_append_homomorphism
M,N:Formula List. 
(M @ N) = (M)+(N) 
list_rank_append_homomorphism
(L) == reduce(
x,y. (x)+y;0;L)
M,N:Formula List. (M @ N) = (M)+(N)
list_rank_append_homomorphism