The Rewster: Type Preserving Rewrite Rules for the Coq Proof Assistant

In dependently typed proof assistants, users can declare axioms to extend the ambient logic locally with new principles and propositional equalities governing them. Additionally, rewrite rules have recently been proposed to allow users to extend the logic with new definitional equalities, enabling t... View More