(8steps total) PrintForm Definitions mb event system 6 Sections EventSystems Search Doc
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: ma-single-pre-init1-feasible 3
1. T : Type
2. T' : Type
3. x : Id
4. T
5. a : Id
6. P : TT'Prop
7. T'
8. u:T. Dec(v:T'. P(u,v))
9. a@0 : Id
10. eqof(IdDeq)(a,a@0)  false
  <[x],x.T>  z:Id fp-> Type
By: Fold `fpf-single` 0

Generated subgoals:

None

About:
pairconsnilbfalseassertdecidablelambdaapply
functionuniversememberpropallexists
IF YOU CAN SEE THIS go to http://www.cs.cornell.edu/Info/People/sfa/Nuprl/Shared/Xindentation_hack_doc.html

(8steps total) PrintForm Definitions mb event system 6 Sections EventSystems Search Doc