Nuprl - Proof: l all cons

(6steps 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 cons

T:Type, P:(T

Prop), x:T, L:T List. (

[x / L].P(y))

P(x) & (

L.P(y))

By:	Unfold `l_all` 0

Generated subgoals:

1 1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. y:T. (y  [x / L])  P(y)
  P(x)
1 step

2 1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. y:T. (y  [x / L])  P(y)
6. y : T
7. (y  L)
  P(y)
1 step

3 1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. P(x)
6. y:T. (y  L)  P(y)
7. y : T
8. (y  [x / L])
  P(y)
3 steps

About:

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

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

1	1. T : Type 2. P : TProp 3. x : T 4. L : T List 5. y:T. (y [x / L]) P(y) P(x)	1 step
2	1. T : Type 2. P : TProp 3. x : T 4. L : T List 5. y:T. (y [x / L]) P(y) 6. y : T 7. (y L) P(y)	1 step
3	1. T : Type 2. P : TProp 3. x : T 4. L : T List 5. P(x) 6. y:T. (y L) P(y) 7. y : T 8. (y [x / L]) P(y)	3 steps