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