Origin
Sections
ClassicalProps(jlc)
Doc
sequent_sat_lemmas
Nuprl Section: sequent_sat_lemmas
Selected Objects
THM
not_sequent_satisfiable_and_falsifiable
S:Sequent, a:Assignment.
(a |= S & a |
S)
S:Sequent, a:Assignment. 
(a |= S & a |
S)S:Sequent, a:Assignment. (a |= S & a | S)