set_option trace.Meta.Tactic.simp.rewrite true in
dsimp [P] -- unfold P, P h ==> h = h
Register as a new user and use Qiita more conveniently
- You get articles that match your needs
- You can efficiently read back useful information
- You can use dark theme