Nuprl - Proof: ma-single-pre-init1-feasible 1

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 1

1. T : Type
2. T' : Type
3. Id
4. T
5. a : Id
6. P : T

Prop
7. T'
8.

u:T. Dec(

v:T'. P(u,v))
9. k : Knd
10. eqof(KindDeq)(locl(a),k)

false

Dec(T')

By:

OrLeft

Generated subgoals:

None

About:

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