(8steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: alle-at-iff
  es:ES, i:Id, P:({e:E| loc(e) = i  Id }Prop).
  e@i.P(e)  e@i.first(e)  P(e) & e@i.first(e)  P(pred(e))  P(e)
By: Auto

Generated subgoals:

1 1. es : ES
2. i : Id
3. P : {e:E| loc(e) = i  Id }Prop
4. e@i.P(e)
  e@i.first(e)  P(e)
1 step
2 1. es : ES
2. i : Id
3. P : {e:E| loc(e) = i  Id }Prop
4. e@i.P(e)
  e@i.first(e)  P(pred(e))  P(e)
1 step
3 1. es : ES
2. i : Id
3. P : {e:E| loc(e) = i  Id }Prop
4. e@i.first(e)  P(e)
5. e@i.first(e)  P(pred(e))  P(e)
  e@i.P(e)
4 steps
4 1. es : ES
2. i : Id
3. {e:E| loc(e) = i  Id }Prop
4. e : {e:E| loc(e) = i  Id }
5. first(e)
  pred(e)  {e:E| loc(e) = i  Id }
1 step

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

(8steps total) PrintForm Definitions Lemmas mb event system 3 Sections EventSystems Doc