diff --git a/wp.v b/wp.v
index 2913853..dde3ed2 100644
--- a/wp.v
+++ b/wp.v
@@ -222,6 +222,12 @@ Proof.
     - simpl. unfold assertImplLogical in impl. apply (impl m). apply conseq.
 Qed.
 
+Lemma interp_of_error (s: Instr):
+    interp s (MemError) = MemError.
+Proof.
+    unfold MemError. destruct s; cbv; trivial.
+Qed.
+
 
 Theorem hoare_provability_implies_consequence :
     forall (pre: Assert), forall (s: Instr), forall (post: Assert),
@@ -229,18 +235,18 @@ Theorem hoare_provability_implies_consequence :
             -> ( |= [| pre |] s [| post |] ) % assert.
 Proof.
     intros pre instr post. intros deduction.
-    induction deduction; intros mem preInMem; simpl.
+    induction deduction; intros mem preInMem.
     - exact preInMem.
-    - trivial.
+    - simpl; trivial.
     - exact preInMem.
     - apply (weaken_in_conseq post' post (interp s (MemElem mem)) H0).
       apply IHdeduction. apply H. exact preInMem.
-    - destruct (interp s1 (MemElem mem)) eqn:mRel.
-        admit.
-        apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
-        specialize IHdeduction1 with mem as IH1_mem.
-        rewrite mRel in IH1_mem. apply IH1_mem. assumption.
-    - destruct (expr mem =? 0)%Z eqn:branchEqn.
+    - simpl; destruct (interp s1 (MemElem mem)) eqn:mRel.
+        * fold MemError. rewrite (interp_of_error s2); simpl; trivial.
+        * apply (IHdeduction2 m). unfold hoare_consequence in IHdeduction1.
+          specialize IHdeduction1 with mem as IH1_mem.
+          rewrite mRel in IH1_mem. apply IH1_mem. assumption.
+    - simpl; destruct (expr mem =? 0)%Z eqn:branchEqn.
         * apply (IHdeduction2 mem). unfold assertOfExpr.
           unfold assertAnd. split.
             + assumption.