IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At:
append assoc12 1. T : Type
2. T List
3. bs : T List
4. cs : T List
5. u : T 6. v : T List
7. ((v @ bs) @ cs) = (v @ bs @ cs)
u.((v @ bs) @ cs) = u.(v @ bs @ cs)
By:
RewriteWith [7] [] 0
Generated subgoals:
None
About:
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
u.((v @ bs) @ cs) = u.(v @ bs @ cs)
