[Agda] Agda implementation of McBride's unification paper?

[Kenichi Asai]

Dear all,

I wonder if there is an agda implementation of Conor McBride's paper
"First-order unification by structural recursion".  Any information is
welcome.

The Data.List.Countdown module in the standard library appears to be
related to the paper.  If there is any document on how to use it,
please let me know.  (I am rather new to agda, and it is a bit
difficult for me to read through the module, although I am trying.)

Thank you in advance!

Sincerely,

-- 
Kenichi Asai