PrintForm Definitions sequent sat lemmas Sections ClassicalProps(jlc) Doc

At: not sequent satisfiable and falsifiable 1 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
7. x: Formula
8. x(eqF) S1
9. a | x

False
By:
Inst Thm* eq:{T=}, P:(TProp), L:T List. xL.P(x) (z:T. z(eq) L P(z)) [Formula;eqF;f. a |= f ;S1]
THEN
Analyze -1
THEN
Thin -1
THEN
RenameVar `h' -5
THEN
With h (Analyze -1)
THEN
Thin -5
Generated subgoal:

16. x: Formula
7. x(eqF) S1
8. a | x
9. z:Formula. z(eqF) S1 a |= z
False

About:
falselistassert