Nuprl - Proof: no repeats mapoutl 2

(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc

1. A: Type
2. B: Type
3. s: (A+B) List
4. u: A+B
5. v: (A+B) List
6. isl(u)
7. no_repeats(A+B;v)
8. (u v)
9. no_repeats(A;mapoutl(v))

(outl(u) mapoutl(v))

By: ParallelOp -2 THEN RWO Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) -1 THEN ExRepD

Generated subgoal:

1 8. no_repeats(A;mapoutl(v))
9. y: A+B
10. (y v)
11. isl(y)
12. outl(u) = outl(y)
(u v) 1 step

About:

(4steps total) PrintForm Definitions Lemmas graph 1 1 Sections Graphs Doc