1. T : Type
2. E : TTProp
3. x,y:T. Dec(E(x,y))
  f:(TT). x,y:T. f(x,y)  E(x,y)

By:	(RenameVar `g' 3) THEN (Unfold `decidable` 3) THEN Witness x,y. InjCase(g(x,y); a. true; b. false) THEN (Reduce 0)

1

3. g : x,y:T. E(x,y)  E(x,y)   x,y:T. InjCase(g(x,y); a. true; b. false)  E(x,y)

12 steps

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