Nuprl - Proof: no repeats mapoutl 2 1

(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. no_repeats(A;mapoutl(v))
9. y: A+B
10. (y v)
11. isl(y)
12. outl(u) = outl(y)

(u v)

By: Analyze 4 THEN All Reduce THEN Try Trivial THEN Analyze -4 THEN All Reduce THEN Try Trivial THEN HypSubst -1 0

Generated subgoals:

None

About:

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