full
assignment
Sections
ClassicalProps(jlc)
Doc
Def
Full(F) == {a:Assignment| a |= F
a |
F }
Thm*
F:Formula, a:Full(F). a |= F
a |
F full_formula_assignment_properties
F:Formula, a:Full(F). a |= F 
a |
F
full_formula_assignment_properties
a | F }
F:Formula, a:Full(F). a |= F a | F
full_formula_assignment_properties