IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
exteq subset vs and1 1. A : Type
2. P : AProp
3. Q : AProp
{x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }
By:
Analyze
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Prop
{x:{x:A| P(x) }| Q(x) } =ext {x:A| P(x) & Q(x) }
