(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: swap adjacent instance
  A:Type, P:(AAProp), X,Y:A List, a,b:A.
  P(a,b)  ((X @ [a; b] @ Y) swap adjacent[P(x,y)] (X @ [b; a] @ Y))
By: Auto THEN Unfold `swap_adjacent` 0 THEN Reduce 0 THEN InstConcl [||X||]

Generated subgoals:

1 1. A : Type
2. P : AAProp
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)
  P((X @ [a; b / Y])[||X||],(X @ [a; b / Y])[(||X||+1)])
6 steps
2 1. A : Type
2. P : AAProp
3. X : A List
4. Y : A List
5. a : A
6. b : A
7. P(a,b)
  (X @ [b; a / Y]) = swap(X @ [a; b / Y];||X||;||X||+1)
19 steps

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

(26steps total) PrintForm Definitions Lemmas mb list 2 Sections MarkB generic Doc