T:Type, a:T, Q:(TProp). (a = !x:T. Q(x))  a  {!x:T | Q(x)}

1

1. T : Type 2. a : T 3. Q : TProp 4. Q(a) 5. a':T. Q(a')  a' = a   a  {x:T| Q(x) & (y:T. Q(y)  y = x) }

2 steps

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