Nuprl - Proof: l all map

(3steps 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: l all map

A,B:Type, f:(A

B), L:A List, P:(B

Prop).

(

map(f;L).P(x))

(

L.P(f(x)))

By:	Unfold `l_all` 0 THEN RWO Thm* a:T List, x:T', f:(TT'). (x map(f;a)) (y:T. (y a) & x = f(y)) 0 THEN ExRepD

Generated subgoals:

1 1. A : Type
2. B : Type
3. f : AB
4. L : A List
5. P : BProp
6. x:B. (y:A. (y  L) & x = f(y))  P(x)
7. x : A
8. (x  L)
  P(f(x))
1 step

2 1. A : Type
2. B : Type
3. f : AB
4. L : A List
5. P : BProp
6. x:A. (x  L)  P(f(x))
7. x : B
8. y : A
9. (y  L)
10. x = f(y)
  P(x)
1 step

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

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

1	1. A : Type 2. B : Type 3. f : AB 4. L : A List 5. P : BProp 6. x:B. (y:A. (y L) & x = f(y)) P(x) 7. x : A 8. (x L) P(f(x))	1 step
2	1. A : Type 2. B : Type 3. f : AB 4. L : A List 5. P : BProp 6. x:A. (x L) P(f(x)) 7. x : B 8. y : A 9. (y L) 10. x = f(y) P(x)	1 step