Nuprl - Proof: mapoutl member

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

A,B:Type, s:(A+B) List, x:A. (x mapoutl(s)) (inl(x) s)

By: RWO Thm* s:(A+B) List, x:A. (x mapoutl(s)) (y:A+B. (y s) & isl(y) & x = outl(y)) 0

Generated subgoals:

1 1. A: Type
2. B: Type
3. s: (A+B) List
4. x: A
5. y:A+B. (y s) & isl(y) & x = outl(y)
(inl(x) s) 1 step

2 1. A: Type
2. B: Type
3. s: (A+B) List
4. x: A
5. (inl(x) s)
y:A+B. (y s) & isl(y) & x = outl(y) 1 step

About:

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

1	1. `A:` `Type` 2. `B:` `Type` 3. `s:` `(A+B) List` 4. `x:` `A` 5. `y:A+B. (y s) & isl(y) & x = outl(y)` `(inl(x) s)`	1 step

2	1. `A:` `Type` 2. `B:` `Type` 3. `s:` `(A+B) List` 4. `x:` `A` 5. `(inl(x) s)` `y:A+B. (y s) & isl(y) & x = outl(y)`	1 step