Nuprl - Pf decidable functionality wrt iff

P,Q:Prop. (P Q) (Dec(P) Dec(Q))

By: Unfolds [`guard`;`decidable`] 0

Generated subgoals:

1 1. P: Prop
2. Q: Prop
3. P Q
4. P Q
5. P P
Q Q

2 1. P: Prop
2. Q: Prop
3. P Q
4. P Q
5. Q Q
P P

About:

1	1. `P:` `Prop` 2. `Q:` `Prop` 3. `P Q` 4. `P Q` 5. `P P` `Q Q`
2	1. `P:` `Prop` 2. `Q:` `Prop` 3. `P Q` 4. `P Q` 5. `Q Q` `P P`