formula list Sections ClassicalProps(jlc) Doc

Def == {i:| 0i }

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

Thm* (Formula List) list_rank_wf

In prior sections: int 1 bool 1 sqequal 1 int 2 list 1 list 3 jlc formula rank