[Agda] cong with wildcard

[Nils Anders Danielsson]

On 10/07/2018 23.11, Matthew Daggitt wrote:
> Also might be worth having a look at Bradley's Agda holes library
> (https://github.com/bch29/agda-holes).

I suspect that this library does not work with the latest (development?)
version of Agda. (Because Holes.Term.⌞_⌟ is inlined. This can be fixed
by using the NOINLINE pragma.)

I have two tactics for automatically generating applications of
cong-like lemmas, one of which is based on Bradley Hardy's idea:

   http://www.cse.chalmers.se/~nad/listings/equality/Tactic.By.html
   git clone http://www.cse.chalmers.se/~nad/repos/equality/

-- 
/NAD