(10steps 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: last with property
  T:Type, L:T List, P:(||L||Prop).
  (x:||L||. Dec(P(x)))
  
  (i:||L||. P(i))  (i:||L||. P(i) & (j:||L||. i<j  P(j)))
By: Auto THEN Inst Thm: interleaving split [T;L;P] THENA Try Trivial THEN ExRepD

Generated subgoal:

1 1. T : Type
2. L : T List
3. P : ||L||Prop
4. x:||L||. Dec(P(x))
5. i : ||L||
6. P(i)
7. L1 : T List
8. L2 : T List
9. f1 : ||L1||||L||
10. f2 : ||L2||||L||
11. interleaving_occurence(T;L1;L2;L;f1;f2)
12. i:||L1||. P(f1(i))
13. i:||L2||. P(f2(i))
14. i:||L||. 
14. (P(i)  (j:||L1||. f1(j) = i)) & (P(i)  (j:||L2||. f2(j) = i))
  i:||L||. P(i) & (j:||L||. i<j  P(j))
9 steps

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

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