PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

At: prop decide 1 1 1 2 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. a: Assignment
7. sL.a | s
8. a | S

|= S (a:Assignment. a | S)
By: Choose [2]
Generated subgoal:

1 a:Assignment. a | S

About:
orexistslistequalint
applynatural_numberimpliesall