[Agda] cong with wildcard

[Sergei Meshveliani]

Dear all,

There is a problem of unnecessary large terms in proofs in a source
program. For example, in an equality proof by EquationalReasoning of 

      begin T1  ≡⟨ cong foo1 eq1 ⟩ 
            T2  ≡⟨ cong foo2 eq2 ⟩
            T3  
            ...
      ∎

foo1, foo2 ...  often occur large terms which can be replaced with `_'.
But Agda cannot solve this.
For example, for the Nat arithmetic, the line

   (a * 1 + 1+m * n)    ≡⟨ cong (_+ (1+m * n)) (Nat0.*1 a) ⟩

means replacing  a * 1  with  a.
And from the term triple

   (a * 1 + 1+m * n)  ,  (cong (_+ _) (Nat0.*1 a)) ,
   (a + 1+m * n)

it is clear (to a human) which term  t  to substitute for `_' in order
to obtain the third term  
-- provided that this  t  is a subterm in (a * 1 + 1+m * n).

More general: the derivation is 

              E1   -- cong (op _) foo  -->
              E2

where op is an operator, and the prover needs to search in E1 all
subterms to which (op X) matches, and which substitution derives E2.
  
Does there exist a library for Agda that has tools for this? 
Can something easy be done towards such a tool?

Regards,

------
Sergei