Inductive Types の Exercises の exponentiation の実装。 色々感じが掴めてきて rw、simp を使わないでかけるようになってきた Eq.refl に何か渡すことで 何か = 何かの評価 の等式が得られる Eq.refl は自動的に解決されるので calc の Eq.refl の行は本…