Nuprl - Proof: l before decomp 1

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

1. T: Type
2. L: T List
3. x: T
4. y: T
5. x before y L

A,B:T List. L = (A @ B) & (x A) & (y B)

By: Unfold `l_before` -1 THEN Lemmaize [-1] THEN InductionOnList

Generated subgoals:

1 x,y:T. [x; y] nil (A,B:T List. nil = (A @ B) & (x A) & (y B)) 1 step

2 3. u: T
4. v: T List
5. x,y:T. [x; y] v (A,B:T List. v = (A @ B) & (x A) & (y B))
x,y:T. [x; y] [u / v] (A,B:T List. [u / v] = (A @ B) & (x A) & (y B)) 7 steps

About:

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

1	`x,y:T. [x; y] nil (A,B:T List. nil = (A @ B) & (x A) & (y B))`	1 step

2	3. `u:` `T` 4. `v:` `T List` 5. `x,y:T. [x; y] v (A,B:T List. v = (A @ B) & (x A) & (y B))` `x,y:T. [x; y] [u / v] (A,B:T List. [u / v] = (A @ B) & (x A) & (y B))`	7 steps