Origin Sections ClassicalProps(jlc) Doc

sequent_valid

Nuprl Section: sequent_valid

Selected Objects
defsequent_valid|= S == a:Full(S). a |= S
THMformula_valid_iff_sequent_validF:Formula. |= F |= < nil,[F] >