1. A : Type
2. B : Type
  f:((A+B)(B+A)), g:((B+A)(A+B)). InvFuns(A+B;B+A;f;g)

By:	Witness: Wie.InjCase(e; x. inr(x); y. inl(y)) | Wie.InjCase(e; x. inr(x); y. inl(y))

1

InvFuns(A+B;B+A   InvFuns;e.InjCase(e; x. inr(x); y. inl(y))   InvFuns;e.InjCase(e; x. inr(x); y. inl(y)))

1 step

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