Proof Repair across Quotient Type Equivalences

Cosmo Viola, Max Fan, Talia Ringer

Proofs in proof assistants like Rocq can be brittle, breaking easily in response to changes. To address this, recent work introduced an algorithm and tool in Rocq to automatically…