Nuprl - Proof: subtype rel dep function

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: subtype rel dep function

A:Type, B:(A

Type), C:Type, D:(C

Type).

r A)

(

a:C. B(a)

r D(a))

((a:A

B(a))

r (c:C

D(c)))

By:	Auto THEN TrySubsume THEN Analyze 0 THEN Analyze 0 THEN TrySubsume THEN DoSubsume THEN BackThruSomeHyp

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html