Nuprl - Proof: all functionality wrt implies

(2steps total) PrintForm core StandardLIB Doc

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: all functionality wrt implies

S,T:Type, P,Q:(S

Prop).

S = T

(

z:S. P(z)

Q(z))

(

x:S. P(x))

(

y:T. Q(y))

By:	Unfold `guard` 0 THEN UnivCD

Generated subgoal:

1 1. S : Type
2. T : Type
3. P : SProp
4. Q : SProp
5. S = T
6. z:S. P(z) Q(z)
7. x:S. P(x)
8. y : T
Q(y)
1 step

About:

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

(2steps total) PrintForm core StandardLIB Doc