Nuprl - Proof: l exists cons

(5steps 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 exists cons

T:Type, P:(T

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

[x / L].P(y))

P(x)

(

L.P(y))

By:	Unfold `l_exists` 0 THEN RWO Thm* l:T List, a,x:T. (x [a / l]) x = a (x l) 0 THEN ExRepD

Generated subgoals:

1 1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. y : T
6. y = x  (y  L)
7. P(y)
  P(x)  (y:T. (y  L) & P(y))
3 steps

2 1. T : Type
2. P : TProp
3. x : T
4. L : T List
5. P(x)  (y:T. (y  L) & P(y))
  y:T. y = x  (y  L) & P(y)
1 step

About:

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

(5steps 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 6. y = x (y L) 7. P(y) P(x) (y:T. (y L) & P(y))	3 steps
2	1. T : Type 2. P : TProp 3. x : T 4. L : T List 5. P(x) (y:T. (y L) & P(y)) y:T. y = x (y L) & P(y)	1 step