[Agda] forced arguments in EqReasoning

[mechvel at scico.botik.ru]

Dear Agda developers,

I am sorry for repeating an issue. It keeps on biting.

The reasoning step of the the kind
               foo + 0  ==  foo + ((- largeExpression) + largeExpression)

is normally coded as
                   +congˡ (=sym (-x+x largeExpression)),

where "-x+x" is a proof for  "forall x -> (- x) + x == 0".

This is sufficient for simple types. For example, for Nat, Integer.
For more complex types, Agda forces me to write this:

   begin⟨ fooSetoid ⟩
     fT + 0ₚ
            ≈⟨ +ₚcongˡ {fT} {0ₚ} {(- largeExpression) + largeExpression} 
$
                 =ₚsym {(- largeExpression) + largeExpression} {0ₚ} $
                 -f+f largeExpression
             ⟩
     fT + ((- largeExpression) + largeExpression)

     ...
   ∎

It this source code,  largeExpression  is written 7 times instead of 3.
And real proofs often contain 5-10 versions of largeExpression that are 
forced to
be copied this way and pollute the source.
This presents a problem:
whether it is possible to invent a tool for deriving such implicits
(and thus to reduce the applied source proofs volume several times).

Regards,

------
Sergei