Nuprl - Proof: fun with inv2 is inj rev

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: fun with inv2 is inj rev

A,B:Type, f:(A

B), g:(B

A). InvFuns(A;B;f;g)

Inj(B; A; g)

By:	Auto THEN Use:[f] BackThru: Thm* InvFuns(A;B;f;g) Inj(A; B; f) THEN BackThru: Thm* InvFuns(A;B;f;g) InvFuns(B;A;g;f)

Generated subgoals:

None

About:

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