(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: pairwise-cons
  T:Type{i}, x:T, L:T List, P:(TTProp{i'}).
  (x,y[x / L].P(x,y))  (x,yL.P(x,y)) & (yL.P(x,y))
By: Auto THEN All (Unfold `pairwise`)

Generated subgoals:

1 1. T : Type{i}
2. x : T
3. L : T List
4. P : TTProp{i'}
5. i:||[x / L]||, j:i. P([x / L][j],[x / L][i])
6. i : ||L||
7. j : i
  P(L[j],L[i])
1 step
2 1. T : Type{i}
2. x : T
3. L : T List
4. P : TTProp{i'}
5. i:||[x / L]||, j:i. P([x / L][j],[x / L][i])
  (yL.P(x,y))
4 steps
3 1. T : Type{i}
2. x : T
3. L : T List
4. P : TTProp{i'}
5. i:||L||, j:i. P(L[j],L[i])
6. (yL.P(x,y))
7. i : ||[x / L]||
8. j : i
  P([x / L][j],[x / L][i])
5 steps

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

(11steps total) PrintForm Definitions Lemmas mb event system 1 Sections EventSystems Doc