Nuprl - Pf append associative 1

(5steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1. T: Type
2. L1: T List
3. L2: T List
4. L3: T List

(L1 @ L2 @ L3) = ((L1 @ L2) @ L3)

By: ListInd 2

Generated subgoals:

1 (nil @ L2 @ L3) = ((nil @ L2) @ L3)

2 5. u: T
6. v: T List
7. (v @ L2 @ L3) = ((v @ L2) @ L3)
((u.v) @ L2 @ L3) = (((u.v) @ L2) @ L3)

About:

(5steps) PrintForm Definitions list 3 jlc Sections Support(jlc) Doc

1	`(nil @ L2 @ L3) = ((nil @ L2) @ L3)`
2	5. `u:` `T` 6. `v:` `T List` 7. `(v @ L2 @ L3) = ((v @ L2) @ L3)` `((u.v) @ L2 @ L3) = (((u.v) @ L2) @ L3)`