Nuprl - Pf formula_valid_iff_sequent

F:Formula. |= F |= < nil,[F] >

By: Repeat (Analyze 0)

Generated subgoals:

1 1. F: Formula
2. |= F
3. a: Full( < nil,[F] > )
a |= < nil,[F] >

2 1. F: Formula
2. |= < nil,[F] >
3. a: Full(F)
a |= F

About:

1	1. `F:` `Formula` 2. `\|= F` 3. `a:` `Full( < nil,[F] > )` `a \|= < nil,[F] >`
2	1. `F:` `Formula` 2. `\|= < nil,[F] >` 3. `a:` `Full(F)` `a \|= F`