IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
ifthenelse distr subtype ooc A:Type, b:, P,Q:(AProp).
{x:A| if bP(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi
By:
SimilarTo
Thm* {x:A| if bP(x) else Q(x) fi }
Thm* =ext
Thm* if b {x:A| P(x) } else {x:A| Q(x) } fi
1. A : Type
2. b : 3. P : AProp
4. Q : AProp
5. {x:A| if bP(x) else Q(x) fi } =ext if b {x:A| P(x) } else {x:A| Q(x) } fi
{x:A| if bP(x) else Q(x) fi } ~ if b {x:A| P(x) } else {x:A| Q(x) } fi
1 step
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html