PrintForm Definitions formula satisfaction Sections ClassicalProps(jlc) Doc

At: decidable formula sat

a:Assignment, f:Formula. Dec(a |= f )
By:
UnivCD
THEN
Unfold `formula_sat` 0
Generated subgoal:

11. a: Assignment
2. f: Formula
Dec((f under a) = 3)

About:
allequal