Nuprl - Pf propositional_decidability 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 (a:Assignment. sL.a | s)

|= S (a:Assignment. a | S)

By: Analyze -1

Generated subgoals:

1 6. sL.|= s
|= S (a:Assignment. a | S)

2 6. a:Assignment. sL.a | s
|= S (a:Assignment. a | S)

About:

1	6. `sL.\|= s` `\|= S (a:Assignment. a \| S)`
2	6. `a:Assignment. sL.a \| s` `\|= S (a:Assignment. a \| S)`