Nuprl - Proof: ifthenelse distr subtype

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

A:Type, b:

, P,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:

UnivCD

Generated subgoal:

1 1. A : Type
2. b :
3. P : AProp
4. Q : AProp
{x:A| if b P(x) else Q(x) fi } =ext if b {x:A| P(x) } else {x:A| Q(x) } fi
3 steps

About:

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