PrintForm Definitions sequent sat lemmas Sections ClassicalProps(jlc) Doc

At: not sequent satisfiable and falsifiable 1 1 1
1. S1: Formula List
2. S2: Formula List
3. a: Assignment
4. FS1.a | F FS2.a |= F
5. FS1.a |= F & FS2.a | F

False
By:
MkDiscreteEq `Formula`
THEN
MoveToHyp 1 -1
THEN
RenameVar `eqF' 1
Generated subgoal:

11. eqF: {Formula=}
2. S1: Formula List
3. S2: Formula List
4. a: Assignment
5. FS1.a | F FS2.a |= F
6. FS1.a |= F & FS2.a | F
False

About:
falselistorand