Example:
For
sym : {A : ๐} โ {x y : A} โ (p : x โก y โ A) โ (y โก x โ ?)
given an expression sym p, currently we have to write
rewrite (_ _ _ _ _ โ) h
to rewrite p via h.
I'd want it to look like this: sym {_} {_} {_} โ instead, or better sym โ (via #10)