PrintForm Definitions sequent valid Sections ClassicalProps(jlc) Doc

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

a |= < nil,[F] >
By:
Analyze -1
THEN
OnHyps [-1;-2] AbReduce
Generated subgoal:

14. True
5. a | F & True
a |= < nil,[F] >

About:
pairnilcons