PrintForm Definitions decidability Sections ClassicalProps(jlc) Doc

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

a:Assignment. a | S
By: Witness a
Generated subgoals:

None

About:
existslistequalintapplynatural_numberimpliesall