A Transfer Tactic for Lean

Zhaoxi Chen, Daniel Raggi

Rewriting in proof assistants spans a strict hierarchy. Equational rewriting substitutes based on extensional equality; subequational rewriting substitutes based on homogeneous rel…