is mentioned by
  Q)  ( P Q) | [squash_functionality_wrt_iff] |
| Q) P Q | [squash_functionality_wrt_implies] |
P2) (Q1 Q2) P1  Q1 P2 Q2 | [or_functionality_wrt_implies] |
Q)  P Q | [not_functionality_wrt_implies] |
 P,Q:(S  Prop).
Thm* S = T (x:S. P(x) Q(x)) ( x:S. P(x)) (y:T. Q(y)) | [exists_functionality_wrt_implies] |
| P,Q:(SProp).
Thm* S = T (z:S. P(z) Q(z)) (x:S. P(x)) (y:T. Q(y)) | [all_functionality_wrt_implies] |
| P2) (Q1 Q2) (P1 Q1) P2 Q2 | [implies_functionality_wrt_implies] |
| P2) (Q1 Q2) ((P1 Q1) (P2 Q2)) | [implies_functionality_wrt_iff] |
| P2) (Q1 Q2) P1 & Q1 P2 & Q2 | [and_functionality_wrt_implies] |
| Q) (Q R) P R | [implies_transitivity] |
| (A B) A & B | [not_over_or_a] |
Try larger context:
StandardLIB
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html