Agda-like Equational Reasoning in Coq using Tactic Notations

January 3, 2020 766 Words