Nuprl - Pf decidable__all_int

1. i:
2. j:
3. F: {i..j}Prop
4. k:{i..j}. Dec(F(k))
5. (k:{i..j}. F(k)) (k:{i..j}. F(k))

(k:{i..j}. F(k)) (k:{i..j}. F(k))

By: Analyze 5

Generated subgoals:

1 5. k:{i..j}. F(k)
(k:{i..j}. F(k)) (k:{i..j}. F(k))

2 5. (k:{i..j}. F(k))
(k:{i..j}. F(k)) (k:{i..j}. F(k))

About:

1	5. `k:{i..j}. F(k)` `(k:{i..j}. F(k)) (k:{i..j}. F(k))`
2	5. `(k:{i..j}. F(k))` `(k:{i..j}. F(k)) (k:{i..j}. F(k))`