Nuprl - Proof: compose append 2 1

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: compose append 2 1

1. T : Type
2. (T

T) List
3. u : T

T
4. v : (T

T) List
5.

L2:(T

T) List. compose_list(v) o compose_list(L2) = compose_list(v @ L2)
6. L2 : (T

T) List
7. compose_list(v) o compose_list(L2) = compose_list(v @ L2)

u o compose_list(v) o compose_list(L2)

By:	Ext THEN Reduce 0

Generated subgoals:

None

About:

IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html