diff --git a/ConcreteSemantics/BigStep.lean b/ConcreteSemantics/BigStep.lean
index f3ba589..7844b97 100644
--- a/ConcreteSemantics/BigStep.lean
+++ b/ConcreteSemantics/BigStep.lean
@@ -69,6 +69,9 @@ inductive BigStep : Stmt → State → State → Prop where
 -- BigStep のための見やすい記法を用意する
 @[inherit_doc] notation:55 "(" S:55 "," s:55 ")" " ==> " t:55 => BigStep S s t
 
+-- BigStep がゴールにある場合にそれを aesop が扱えるようにする
+attribute [aesop safe constructors] BigStep
+
 /-- `sillyLoop` コマンドにより、`x = 1, y = 0` という状態は `x = y = 0` という状態に変わる。 -/
 example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
   -- sillyLoop の定義を展開する
@@ -79,14 +82,9 @@ example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
   apply BigStep.while_true
 
   -- 条件式 `x > y` が真であること
-  case hcond =>
-    simp
+  case hcond => simp
 
-  case hbody =>
-    -- `;` でつながっているのを分解する
-    apply BigStep.seq
-    · apply BigStep.skip
-    · apply BigStep.assign
+  case hbody => aesop
 
   case hrest =>
     simp only [gt_iff_lt, ↓reduceIte, Nat.sub_self]
@@ -97,8 +95,7 @@ example : (sillyLoop, (fun _ ↦ 0)["x" ↦ 1]) ==> (fun _ ↦ 0) := by
 
     -- このとき状態は `x ↦ 0, y ↦ 0` なので条件式は偽。
     -- したがって while_false を使う
-    apply BigStep.while_false
-    simp
+    apply BigStep.while_false (hcond := by simp)
 
 /- ### 7.2.2 Deriving IMP Executions -/
 
@@ -111,4 +108,4 @@ example (s : State) : (set_to_five, s) ==> (s["x" ↦ 5]["y" ↦ 5]) := by
   -- set_to_five の定義を展開する
   dsimp [set_to_five]
 
-  apply BigStep.seq <;> apply BigStep.assign
+  aesop
diff --git a/ConcreteSemantics/Equivalence.lean b/ConcreteSemantics/Equivalence.lean
index 2f733a6..c0d8345 100644
--- a/ConcreteSemantics/Equivalence.lean
+++ b/ConcreteSemantics/Equivalence.lean
@@ -37,7 +37,7 @@ instance : Setoid Stmt where
 /-- `≈` 記号の中身を展開するタクティク -/
 syntax "unfold" "≈" : tactic
 macro_rules
-  | `(tactic|unfold ≈) => `(tactic|dsimp only [(· ≈ ·), Setoid.r, equivCmd])
+  | `(tactic|unfold ≈) => `(tactic| dsimp only [(· ≈ ·), Setoid.r, equivCmd])
 
 /-- ### Lemma 7.3
 `while` 文の意味は、
@@ -84,9 +84,7 @@ theorem while_congr {B : State → Prop} {c c' : Stmt} {s t : State} (h : c ≈
   induction h_while <;> cases hx
 
   -- 条件式が偽の場合
-  case while_false s' hcond =>
-    apply BigStep.while_false
-    assumption
+  case while_false s' hcond => aesop
 
   -- 条件式が真の場合
   case while_true s' t' u' hcond' hbody' _ _hrest ih =>
@@ -123,14 +121,12 @@ theorem while_eq_of_eq (B : State → Prop) (c c' : Stmt) (h : c ≈ c') : while
     specialize h s w
 
     -- aesop で片を付ける
-    aesop
     all_goals sorry
 
   case mpr =>
     -- whileDo の定義を展開する
     rw [while_iff]
     -- aesop で片を付ける
-    aesop
     sorry
 
 end BigStep
diff --git a/ConcreteSemantics/RuleInversion.lean b/ConcreteSemantics/RuleInversion.lean
index 24916f1..c0d9047 100644
--- a/ConcreteSemantics/RuleInversion.lean
+++ b/ConcreteSemantics/RuleInversion.lean
@@ -22,7 +22,7 @@ namespace BigStep
     -- s = t なので、BigStep.skip の定義から従う
     rw [h]
 
-    apply BigStep.skip
+    aesop
 
 /-- seq に関する inversion rule -/
 @[simp] theorem seq_iff {S T s u} :
@@ -40,9 +40,7 @@ namespace BigStep
   -- 右から左を示す
   case mpr =>
     obtain ⟨t, hS, hT⟩ := h
-
-    -- big_step タクティクを使わない証明
-    apply BigStep.seq <;> assumption
+    aesop
 
 /-- if に関する inversion rule -/
 @[simp] theorem if_iff {B S T s t} : (ifThenElse B S T, s) ==> t ↔
diff --git a/ConcreteSemantics/Tactic/BigStep.lean b/ConcreteSemantics/Tactic/BigStep.lean
deleted file mode 100644
index aedc3bc..0000000
--- a/ConcreteSemantics/Tactic/BigStep.lean
+++ /dev/null
@@ -1,36 +0,0 @@
-import ConcreteSemantics.BigStep
-
-/-! BigStep の形をしたゴールを証明するタクティク `big_step` を定義する
-
-便利なタクティクを作ろうとおもったが、デバッグが思ったより大変だったので後回しになっている。 -/
-
-/-- `(S, s) ==> t` の形をしたゴールを示すためのタクティク -/
-syntax "big_step" : tactic
-
--- 以下の変換ルールは下から順番に試されてゆき、失敗した時点で次のものに移る。成功したときに展開先が確定する
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.skip)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.assign)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.seq)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.seq (by assumption) (by assumption))
-
--- hcond を引数として渡して apply することにより、
--- if_true を使うべき場面で if_false へ展開してしまうバグを防止している
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.if_true (hcond := by assumption) <;> assumption)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.if_false (hcond := by assumption) <;> assumption)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.while_true (hcond := by assumption) <;> try simp_all)
-
-macro_rules
-  | `(tactic| big_step) => `(tactic| apply BigStep.while_false (hcond := by assumption) <;> try simp_all)