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