依存関係のある値のうちの一部をrewriteしようとしたときの問題 - にわとり小屋でのプログラミング ブログ をAgdaで書くとどうなるか． こういうことだろうか？ module AC-2013-5 where open import Data.Nat import Relation.Binary.PropositionalEquality …