1. es : ES
2. e : E
3. e' : E
4. v : the_es:ES, e',e:E. Dec(e  e' )
  InjCase(v(es,e',e); x. true, false)  e  e' 

1

4. the_es:ESe',e:EDec(e  e' ) 5. v1 : Dec(e  e' )   InjCase(v1; x. true, false)  e  e'

2 steps

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