Nuprl - Proof: alle-at-iff 2

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

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

Prop
4.

e@i.P(e)

e@i.

first(e)

P(pred(e))

P(e)

By:	RepeatFor 3 (ParallelOp -1) THEN Analyze THEN EsAuto

Generated subgoals:

None

About:

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