Thm* a:Assignment, F:Formula. (F under a) valuation_wf

In prior sections: assignment