Origin
Sections
ClassicalProps(jlc)
Doc
sequent_valid
Nuprl Section: sequent_valid
Selected Objects
def
sequent_valid
|= S ==
a:Full(S). a |= S
THM
formula_valid_iff_sequent_valid
F:Formula. |= F
|= < nil,[F] >