IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
iseg transitivity11 1. T : Type
2. l1 : T List
3. l2 : T List
4. l3 : T List
5. l4 : T List
6. l2 = (l1 @ l4)
7. l : T List
8. l3 = (l2 @ l)
((l1 @ l4) @ l) = (l1 @ l4 @ l)
By:
Easy
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
((l1 @ l4) @ l) = (l1 @ l4 @ l)
