Implement "dot patterns" in rewrite

[Russoul]

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)