<div dir="ltr">I&#39;m pretty new to Agda, so I apologize for this newbie question.<div><br></div><div>I think it&#39;s pretty cool how Agda can rewrite parts of the AST (I suppose these are &quot;terms&quot;? But I think of it as the AST) using the basic rules of evaluation and normalization. That is, pattern matching on _≡_ introduces new definitional equalities that cause the LHS to reduce to the RHS, without introducing any new machinery. That&#39;s very neat.</div><div><br></div><div>I am, however, wondering if it is necessary. Supposing I had a &quot;macro&quot; (I put &quot;macro&quot; in quotes because I do not mean a standard Agda macro. If I understand correctly, standard Agda macros operate on normalized (open) terms, whereas I mean a procedure that operates on potentially unnormalized (open) terms) that substituted part of the current AST with another part, using a substitution that happened to be available as an equality of some sort.</div><div><br></div><div>What I have in my head is a graphical utility that would show you the current AST as a tree. First, you could direct the utility to perform some reductions (as desired), but not necessarily a full normalization. Then, you could then click on a subtree, and say &quot;replace this with an equivalent expression&quot;, and it would do that (assuming you had access to a proof of that equivalence). My motivation for thinking about this kind of utility are the various hoops that are sometimes required (eg inspect) to convince Agda to rewrite just the part of the AST that is desired. Also, Aaron Stump&#39;s latest post makes it seem like directing rewrites towards particular terms is sometimes a little tricky.</div><div><br></div><div>I am wondering if there are any obvious contradictions or weird behaviors that would turn up as a result of a more general rewrite facility that wasn&#39;t based on reductions. In other words, is there something about handling propositional equalities via reduction that avoids potential pitfalls? Or, put another way, is the principle that &quot;equals may be substituted for equals&quot; generally true in Agda, or does Agda take special care through normalization to make sure that that stays true?</div></div>