Nuprl - Proof: l before decomp 1 2 2

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

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))
6. x: T
7. y: T
8. [x; y] v

A,B:T List. [u / v] = (A @ B) & (x A) & (y B)

By: InstHyp [x;y] 5 THEN ExRepD THEN InstConcl [[u / A];B] THEN Reduce 0

Generated subgoals:

1 9. A: T List
10. B: T List
11. v = (A @ B)
12. (x A)
13. (y B)
[u / v] = [u / (A @ B)] 1 step

2 9. A: T List
10. B: T List
11. v = (A @ B)
12. (x A)
13. (y B)
(x [u / A]) 1 step

About:

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

1	9. `A:` `T List` 10. `B:` `T List` 11. `v = (A @ B)` 12. `(x A)` 13. `(y B)` `[u / v] = [u / (A @ B)]`	1 step

2	9. `A:` `T List` 10. `B:` `T List` 11. `v = (A @ B)` 12. `(x A)` 13. `(y B)` `(x [u / A])`	1 step