PrintForm Definitions sequent valid Sections ClassicalProps(jlc) Doc

At: formula valid iff sequent valid 2 1 2
1. F: Formula
2. a: Full(F)
3. a |= < nil,[F] >

a |= F
By:
UnfoldTopAb -1
THEN
AbReduce -1
Generated subgoal:

13. False a |= F False
a |= F

About:
pairnilcons