[Agda] Converting a pattern match to an equality

[Will Sonnex]

Is there a way to get the current branch of a pattern match in the
form of an equality?

For example:

f with t
... | k = let h : t ≡ k
                h = ?


Cheers,

Will