formula list Sections ClassicalProps(jlc) Doc

Def as @ bs == Case of as; nil bs ; a.as' a.(as' @ bs) (recursive)

Thm* M,N:Formula List. (M @ N) = (M)+(N) list_rank_append_homomorphism

In prior sections: list 1 list 3 jlc