Nuprl - Proof: alle-at-iff 4

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: alle-at-iff 4

1. es : ES
2. i : Id
3. {e:E| loc(e) = i }

Prop
4. e : {e:E| loc(e) = i }
5.

first(e)

pred(e)

{e:E| loc(e) = i

Id }

By:	Analyze -2 THEN Analyze THEN RWO Thm* the_es:ES, e:E. first(e) loc(pred(e)) = loc(e) Id 0

Generated subgoals:

None

About:

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