Nuprl - Proof: equal appends 2

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1. T: Type
2. a: T List
3. u: T
4. v: T List
5. c,b,d:T List. (v @ b) = (c @ d) (e:T List. v = (c @ e) & d = (e @ b) c = (v @ e) & b = (e @ d))

c,b,d:T List. [u / (v @ b)] = (c @ d) (e:T List. [u / v] = (c @ e) & d = (e @ b) c = [u / (v @ e)] & b = (e @ d))

By: InductionOnList THEN Reduce 0

Generated subgoals:

1 6. c: T List
b,d:T List. [u / (v @ b)] = d (e:T List. [u / v] = e & d = (e @ b) nil = [u / (v @ e)] & b = (e @ d)) 1 step

2 6. c: T List
7. u1: T
8. v1: T List
9. b,d:T List. [u / (v @ b)] = (v1 @ d) (e:T List. [u / v] = (v1 @ e) & d = (e @ b) v1 = [u / (v @ e)] & b = (e @ d))
b,d:T List. [u / (v @ b)] = [u1 / (v1 @ d)] (e:T List. [u / v] = [u1 / (v1 @ e)] & d = (e @ b) [u1 / v1] = [u / (v @ e)] & b = (e @ d)) 1 step

About:

(5steps total) PrintForm Definitions graph 1 1 Sections Graphs Doc

1	6. `c:` `T List` `b,d:T List. [u / (v @ b)] = d (e:T List. [u / v] = e & d = (e @ b) nil = [u / (v @ e)] & b = (e @ d))`	1 step

2	6. `c:` `T List` 7. `u1:` `T` 8. `v1:` `T List` 9. `b,d:T List. [u / (v @ b)] = (v1 @ d) (e:T List. [u / v] = (v1 @ e) & d = (e @ b) v1 = [u / (v @ e)] & b = (e @ d))` `b,d:T List. [u / (v @ b)] = [u1 / (v1 @ d)] (e:T List. [u / v] = [u1 / (v1 @ e)] & d = (e @ b) [u1 / v1] = [u / (v @ e)] & b = (e @ d))`	1 step