Nuprl - Proof: card settype

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: card settype

A,A':Type, B:(A

Prop), B':(A'

Prop), f:(A

A').

Bij(A; A'; f)

(

x:A. B(x)

B'(f(x)))

({x:A| B(x) } ~ {x:A'| B'(x) })

By:

Auto

Generated subgoal:

1 1. A : Type
2. A' : Type
3. B : AProp
4. B' : A'Prop
5. f : AA'
6. Bij(A; A'; f)
7. x:A. B(x) B'(f(x))
{x:A| B(x) } ~ {x:A'| B'(x) }
22 steps

About:

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