Thm* M,N:Formula List.
(M @ N) =
(M)+
(N)
list_rank_append_homomorphism
Thm*
(Formula List)
list_rank_wf
In prior sections: formula valuation formula satisfaction formula falsification formula rank formula equality sat lemmas full assignment formula validity sequent