A,A':Type, B:(AProp), B':(A'Prop), f:(AA').
  Bij(A; A'; f)
  
  (x:A. B(x)  B'(f(x)))  ({x:A| B(x) } ~ {x:A'| B'(x) })

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) }

2 steps

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