Nuprl - Proof: one one corr fams if one one corr B 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: one one corr fams if one one corr B 1

1. A : Type
2. B : A

Type
3. B' : A

Type
4.

x:A. B(x) ~ B'(x)

(x:A. B(x)) ~ (x:A. B'(x))

By:	Witness: Id \| Id THEN Reduce 0

Generated subgoal:

1 F:(x:AB(x)B'(x)), G:(x:AB'(x)B(x)).
InvFuns(A;A;Id;Id) & (u:A. InvFuns(B(u);B'(u);F(u);G(u)))
4 steps

About:

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