sequent
valid
Sections
ClassicalProps(jlc)
Doc
Def
|= S ==
a:Full(S). a |= S
Thm*
F:Formula. |= F
|= < nil,[F] > formula_valid_iff_sequent_valid
F:Formula. |= F 
|= < nil,[F] >
formula_valid_iff_sequent_valid
a:Full(S). a |= S
F:Formula. |= F |= < nil,[F] >
formula_valid_iff_sequent_valid