diff --git a/src/axiomatic/GsimM.v b/src/axiomatic/GsimM.v
index fe91c15..c3ac04b 100644
--- a/src/axiomatic/GsimM.v
+++ b/src/axiomatic/GsimM.v
@@ -1054,7 +1054,7 @@ red; splits; try done.
        red; splits; eauto.
        eby eapply no_rmw_from_init.
        eby eapply rmw_acta.
-    + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; subst z0 z b a; left.
+    + unfold singl_rel, sb_ext, eqv_rel, seq in *; desf; eauto; left.
        eapply SB_AT_END; eauto.
        by left; congr.
        eby destruct SB3; subst.
diff --git a/src/axiomatic/GstepWrite.v b/src/axiomatic/GstepWrite.v
index 11c2afa..1fdd54c 100644
--- a/src/axiomatic/GstepWrite.v
+++ b/src/axiomatic/GstepWrite.v
@@ -399,10 +399,10 @@ Proof.
   rewrite gstep_urr_write; try edone; relsimp.
   rewrite gstep_sb_ext_helper_w2; ins.
   split; repeat apply inclusion_union_l; eauto 12 with rel.
-    red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]);
+  red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]);
     by right; eauto.
-  rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. 
-  subst y; splits; ins; tauto.
+  rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; 
+  ins; desf; splits; auto.
 Qed.
 
 Lemma gstep_c_rel_rwr_write l l' :
@@ -416,10 +416,10 @@ Proof.
   rewrite gstep_rwr_write; try edone; relsimp.
   rewrite gstep_sb_ext_helper_w2; ins.
   split; repeat apply inclusion_union_l; eauto 12 with rel.
-    red; unfold seq, eqv_rel; ins; desf; try (by destruct a as [??[]]);
+    red; unfold seq, eqv_rel; ins; desf; try (by destruct y as [??[]]);
     by right; eauto.
   rewrite <- inclusion_union_r2, !eqv_join; unfold eqv_rel; red; ins; desf. 
-  subst y; splits; ins; tauto.
+  splits; auto.
 Qed.
 
 Lemma gstep_t_rel_urr_write l' l x :
diff --git a/src/axiomatic/MsimG.v b/src/axiomatic/MsimG.v
index f8d4471..d8db1ea 100644
--- a/src/axiomatic/MsimG.v
+++ b/src/axiomatic/MsimG.v
@@ -341,7 +341,7 @@ Proof.
   intros K K'; cdes GSTEP; desf; ins; desf.
   by cdes WF'; exfalso; eapply WF_MO; eauto.
   assert (P: is_proper y).
-    by eapply no_mo_to_init; eauto.
+    by eapply no_mo_to_init with (mo:=mo0); eauto.
   destruct (classic (exists x : event, (rf;; rmw) x y)) as [C|]; desc; eauto.
   assert (INx: In x acts).
     by eapply seq_doma in C; [|eapply rf_acta]; eauto.