PrintForm Definitions sequent sat lemmas Sections ClassicalProps(jlc) Doc

At: not sequent satisfiable and falsifiable 1 1 1 1 1 1
1. eqF: {Formula=}
2. S1: Formula List
3. S2: Formula List
4. a: Assignment
5. FS1.a | F
6. FS1.a |= F

False
By:
Using [`eq',eqF] (FwdThru Thm* eq:{T=}, P:(TProp), L:T List. (x:T. x(eq) L & P(x)) yL.P(y) [-2])
THEN
Analyze -1
THEN
Analyze -1
Generated subgoal:

17. x: Formula
8. x(eqF) S1
9. a | x
False

About:
falselist