<div dir="ltr">Hello Agda Community!<br><br>My name is Victor and I&#39;m writing to introduce you guys to <br>something that came out of my (ongoing) MSc project.<br>We wrote a library to perform rewrites, similar to &quot;setoid_rewrite&quot; in Coq.<br><br>The library is available at <a href="https://github.com/VictorCMiraldo/agda-rw" target="_blank">https://github.com/VictorCMiraldo/agda-rw</a> .<br><br>There are a few examples here and there (a 2 min reading of the repo top-page<br>should direct you where you want to go), but here&#39;s a preview of list concatenation<br>associativity, using the tactic &#39;by&#39;:<br><div style="margin-left:40px"><br><br>open import Data.List<br>open import RW.Strategy.PropEq<br>open import <a href="http://RW.RW" target="_blank">RW.RW</a> (≡-strat ∷ [])<br><br>++-assoc : ∀{a}{A : Set a}(xs ys zs : List A)  <br>         → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs)<br>++-assoc [] ys zs       = refl<br>++-assoc (x ∷ xs) ys zs = tactic (by (quote ++-assoc))<br><br></div>The term produced by &#39;by&#39; is<br><div><div style="margin-left:40px"><br></div><div style="margin-left:40px">cong (_::_ x) (++-assoc xs ys zs)<br></div><br>Feel free to experiment with it, note that this is still work-in-progress, though.<br><br>I hope you&#39;ll enjoy it.<br>Best,<br>Victor</div></div>