Oh, I am quite sure there are inefficiencies! Just that they are not entirely inefficiencies.

I have used Fable for formalisation and it will, unless I catch it, reprove results it previously had proven, inline, in other results.