{tactic}`rw`{lit}`  [t]  `{kw}`at`{lit} h` applies th

test