(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 3 2 1

1. T : Type
2. x : T
3. L : T List
4. P : TTProp
5. i:||L||, j:iP(L[j],L[i])
6. (yL.P(x,y))
7. i : ||[x / L]||
8. j : i
9. j = 0
  P(L[(j-1)],L[(i-1)])


By: BackThruSomeHyp


Generated subgoals:

None

About:
listconsintnatural_numbersubtractfunctionuniverseequalpropall
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