diff --git a/_CoqProject b/_CoqProject
index 2bd0138..0a5999b 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -3,6 +3,7 @@ theories/Dec.v
 theories/Eq.v
 theories/ListExt.v
 theories/PrimitiveSegment.v
+theories/AdmissibilityPreservation.v
 theories/Main.v
 theories/Example2.v
 theories/Example3.v
diff --git a/coq-scurve.opam b/coq-scurve.opam
index 48f13f9..3f41ee6 100644
--- a/coq-scurve.opam
+++ b/coq-scurve.opam
@@ -8,8 +8,11 @@ dev-repo: "git+https://github.com/proof-ninja/coq-scurve"
 
 
 depends: [
-  "rocq-prover"
-  "rocq-equations"
+  "rocq-prover" {>= "9.0.0" & < "9.1~"}
+  "rocq-core" {>= "9.0.0" & < "9.1~"}
+  "rocq-runtime" {>= "9.0.0" & < "9.1~"}
+  "coq-core" {>= "9.0.0" & < "9.1~"}
+  "rocq-equations" {>= "1.3" & < "1.4~"}
 ]
 
 authors: [
diff --git a/theories/AdmissibilityPreservation.v b/theories/AdmissibilityPreservation.v
new file mode 100644
index 0000000..9ca9371
--- /dev/null
+++ b/theories/AdmissibilityPreservation.v
@@ -0,0 +1,28 @@
+Require Import Admissible.
+Require Import Reduction.
+
+(* 補題: Ruleを部分リストに適用しても許容性が保たれる *)
+Axiom AdmissibleDirs_sublist_rule: forall l ds ds' r,
+  Rule ds ds' -> AdmissibleDirs (l ++ ds ++ r) -> AdmissibleDirs (l ++ ds' ++ r).
+
+Lemma AdmissibleDirsStep_preserve ds ds' : AdmissibleDirs ds -> ReduceDirStep ds ds' -> AdmissibleDirs ds'.
+Proof.
+  intros AD RDS.
+  (* ReduceDirStep の定義から、l, r, es, es' と Rule es es' が存在する *)
+  inversion RDS as [l r es es' HRule Hds Hds'].
+  (* ds = l ++ es ++ r, ds' = l ++ es' ++ r である *)
+  subst ds ds'.
+  eapply AdmissibleDirs_sublist_rule; eauto.
+Qed.
+
+Lemma AdmissibleDirs_preserve ds ds': AdmissibleDirs ds -> ReduceDir ds ds' -> AdmissibleDirs ds'.
+Proof.
+  intros AD RD.
+  induction RD as [ds | ds ds' ds'' RDS RD IHRD].
+  - (* RDRefl: ds = ds なので自明 *)
+    exact AD.
+  - (* RDTrans: ds -> ds' -> ds'' の場合 *)
+    apply AdmissibleDirsStep_preserve with (ds := ds) in RDS; [|exact AD].
+    apply IHRD.
+    exact RDS.
+Qed.
diff --git a/theories/Admissible.v b/theories/Admissible.v
index 3138e12..fa4dc99 100644
--- a/theories/Admissible.v
+++ b/theories/Admissible.v
@@ -68,9 +68,6 @@ Qed.
 
 Definition reduced ds dsr:= ReduceDir ds dsr /\ ~ CanReduceDirStep dsr. 
 
-Lemma AdmissibleDirs_preserve ds ds': AdmissibleDirs ds -> ReduceDir ds ds' -> AdmissibleDirs ds'.
-Admitted.
-
 Axiom inadmissible_rotation_dif_four: forall ds, Z.abs(rotation_difference ds) >= 4 -> ~ AdmissibleDirs ds.
 
 Lemma repeat_dif_P n: rotation_difference (repeat Plus n) = Z.of_nat n.