Nuprl - Proof: l before append iff 1 2

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

1. T: Type
2. A: T List
3. B: T List
4. x: T
5. y: T
6. u: T
7. v: T List
8. B': T List
9. [x; y] = [u / (v @ B')]
10. [u / v] A
11. B' B

[x; y] A [x; y] B (x A) & (y B)

By: Analyze -5 THEN All Reduce

Generated subgoals:

1 7. B': T List
8. [x; y] = [u / B']
9. [u] A
10. B' B
[x; y] A [x; y] B (x A) & (y B) 1 step

2 7. u1: T
8. v1: T List
9. B': T List
10. [x; y] = [u; u1 / (v1 @ B')]
11. [u; u1 / v1] A
12. B' B
[x; y] A [x; y] B (x A) & (y B) 2 steps

About:

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

1	7. `B':` `T List` 8. `[x; y] = [u / B']` 9. `[u] A` 10. `B' B` `[x; y] A [x; y] B (x A) & (y B)`	1 step

2	7. `u1:` `T` 8. `v1:` `T List` 9. `B':` `T List` 10. `[x; y] = [u; u1 / (v1 @ B')]` 11. `[u; u1 / v1] A` 12. `B' B` `[x; y] A [x; y] B (x A) & (y B)`	2 steps