diff --git a/cs3234/labs/term-project.v b/cs3234/labs/term-project.v
index 9ed317e..f5658d2 100644
--- a/cs3234/labs/term-project.v
+++ b/cs3234/labs/term-project.v
@@ -659,25 +659,44 @@ Qed.
 
 Proposition about_fetch_decode_execute_loop :
   forall (bci1s bci2s : list byte_code_instruction)
-    (ds ds' : data_stack),
-    fetch_decode_execute_loop bci1s ds = OK ds' ->
-    fetch_decode_execute_loop (bci1s ++ bci2s) ds =
-      fetch_decode_execute_loop bci2s (ds').
+    (ds : data_stack),
+    (forall (ds' : data_stack),
+        fetch_decode_execute_loop bci1s ds = OK ds' ->
+        fetch_decode_execute_loop (bci1s ++ bci2s) ds = fetch_decode_execute_loop bci2s (ds'))
+    /\
+    (forall (s : string),
+        fetch_decode_execute_loop bci1s ds = KO s ->
+        fetch_decode_execute_loop (bci1s ++ bci2s) ds = KO s).
 Proof.
-  intros bci1s.
-  induction bci1s as [ | bci bci1s' IHbci1s' ]; intros bci2s ds ds' H_fdel.
-  - rewrite -> fold_unfold_list_append_nil.
-    rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
-    injection H_fdel as ds_eq_ds'.
-    rewrite -> ds_eq_ds'.
-    reflexivity.
-  - rewrite -> fold_unfold_list_append_cons.
-    rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
-    rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
-    case (decode_execute bci ds) as [ ds1 | s ] eqn:H_decode_execute.
-    + rewrite -> (IHbci1s' bci2s ds1 ds' H_fdel).
+  intros bci1s bci2s.
+  induction bci1s as [ | bci bci1s' IHbci1s' ]; intros ds.
+  - split.
+    + intros ds' H_fdel.
+      rewrite -> fold_unfold_list_append_nil.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
+      injection H_fdel as ds_eq_ds'.
+      rewrite -> ds_eq_ds'.
       reflexivity.
-    + discriminate H_fdel.
+    + intros s H_fdel.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_nil in H_fdel.
+      discriminate H_fdel.
+  - split.
+    + intros ds' H_fdel.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
+      case (decode_execute bci ds) as [ ds1 | s ] eqn:H_decode_execute.
+      * destruct (IHbci1s' ds1) as [IH_ok  _].
+        exact (IH_ok ds' H_fdel).
+      * discriminate H_fdel.
+    + intros s H_fdel.
+      rewrite -> fold_unfold_list_append_cons.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_cons.
+      rewrite -> fold_unfold_fetch_decode_execute_loop_cons in H_fdel.
+      case (decode_execute bci ds) as [ ds1 | s1 ] eqn:H_decode_execute.
+      * destruct (IHbci1s' ds1) as [_  IH_ko].
+        exact (IH_ko s H_fdel).
+      * exact H_fdel.
 Qed.
 
 (* ********** *)