PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: propositional decidability 1 1 1 1 1
1. S: Sequent
2. L: Sequent List
3. sL.((s) = 0)
4. sL.|= s |= S
5. a:Assignment. sL.a | s a | S
6. sL.|= s
7. |= S

|= S (a:Assignment. a | S)
By: Choose [1]
Generated subgoals:

None

About:
orexistslistequalint
applynatural_numberimpliesall