This is helpful when defining auto-implicits of the form:
pairEqF : DecEq a
=> (thisX, x, y : a)
-> {prfRefl : Equal x thisX}
-> (prfEq : decEq x thisX = Yes prfRefl)
=> Pair a a
pairEqF thisX x y {prfRefl} {prfEq} = MkPair x y
before auto-implicit search would fail to find `Refl` for `prfRefl`.
With this fix the solution is found.
This fix means we can avoid having to write the following.
pairEqF' : DecEq a
=> (thisX, x, y : a)
-> (prfEq : decEq x thisX = Yes (the (Equal x x) Refl))
=> Pair a a
pairEqF' thisX x y {prfEq} = MkPair x y
I'm playing with some linear structures and finding these useful a lot,
so good to have a consistent syntax for it. '#' is chosen because it's
short, looks a bit like a cross if you look at it from the right angle
(!) and so as not to clash with '@@' in preorder reasoning syntax.
