'a:Type, P:('aType), x:'a.
  P(x)  (y:'a. P(y)  x = y)  (@y:'a. P(y)) = x

1

1. 'a : Type 2. P : 'aType 3. x : 'a 4. P(x) 5. y:'a. P(y)  x = y   InjCase(lem({y:'a| P(y) }); y. y, arb('a)) = x

4 steps

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