(@@) : (t : a) -> (u : a ** t = u)
Until Idris2 supports the 'with (...) proof p' construct, here's a poor-man's replacement.