Nuprl - Proof: l before decomp 1 2

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

At: l before decomp 1 2

1. T: Type
2. L: T List
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))

By: RWO Thm* x1,x2:T, L1,L2:T List. [x1 / L1] [x2 / L2] x1 = x2 & L1 L2 [x1 / L1] L2 0 THEN Analyze -1

Generated subgoals:

1 6. x: T
7. y: T
8. x = u & [y] v
A,B:T List. [u / v] = (A @ B) & (x A) & (y B) 3 steps

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

About:

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