“These linear scripts are unreadable unless replayed step-by-step in the proof assistant.” +1. Elementary tactics killed readability in Coq. Not to mention that you must learn dozens (hundreds?) little tactics. Lambda-calculus is shorter. However, advanced tactics, like “ring”, are useful.

@Qiaochu Yuan: Thanks, I did not know that. I have removed “ct.”.

@Todd Trimble: BTW, Emil's answer would be great if I could understand it. :)

@Todd Trimble: Not so slightly. Emil does not mention any adjunction, and I do not mention atomic=positive diagrams and associative algebras. I posted my answer because I could not follow Emil's answer because of a couple of unfamiliar terms. (Never heard of atomic=positive diagrams before. Now I see they are probably related to $\eta(R)$, though do not see how until I find the precise definition.) And I gave the reference. It is always good to know your predecessors and not to reinvent the wheel. :)