1 files changed, 14 insertions, 0 deletions
diff --git a/backend/CSE3analysisproof.v b/backend/CSE3analysisproof.v
index a012771c..29d171eb 100644
--- a/backend/CSE3analysisproof.v
+++ b/backend/CSE3analysisproof.v
@@ -1341,6 +1341,20 @@ Section SOUNDNESS.
     unfold sem_rel in REL.
     eapply REL; eassumption.
   Qed.
+
+  Lemma apply_cond_sound :
+    forall pc cond args rel rs m
+      (COND : (eval_condition cond (rs ## args) m) = Some true)
+      (REL : (sem_rel rel rs m)),
+      (sem_rel_b (apply_cond (ctx:=ctx) pc cond args rel) rs m).
+  Proof.
+    unfold apply_cond.
+    intros.
+    pose proof (apply_cond1_sound pc cond args rel rs m COND REL) as SOUND1.
+    destruct apply_cond1 eqn:COND1.
+    { apply apply_cond0_sound; auto. }
+    exact SOUND1.
+  Qed.
   
   (*
   Section INDUCTIVENESS.