Nuprl - Proof: ifthenelse distr subtype 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ifthenelse distr subtype 1

1. A : Type
2. b :

3. P : A

Prop
4. Q : A

Prop

{x:A| if b

P(x) else Q(x) fi } =ext if b

{x:A| P(x) } else {x:A| Q(x) } fi

By:	SplitOnConclITE

Generated subgoals:

1 5. b
{x@0:A| P(x@0) } =ext {x:A| P(x) }
1 step

2 5. b
{x:A| Q(x) } =ext {x:A| Q(x) }
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

1	5. b {x@0:A\| P(x@0) } =ext {x:A\| P(x) }	1 step
2	5. b {x:A\| Q(x) } =ext {x:A\| Q(x) }	1 step