diff --git a/opam b/opam
index 639056c099280d9361896f94c278ddc98f8d7e19..d1122910e303df7217349f6e968611d1ebf479ce 100644
--- a/opam
+++ b/opam
@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/igps" ]
 depends: [
-  "coq-iris" { (= "branch.gen_proofmode.2018-06-15.3.d88d654b") | (= "dev") }
+  "coq-iris" { (= "branch.gen_proofmode.2018-06-21.2.8ca8b776") | (= "dev") }
 ]
diff --git a/theories/lang/base.v b/theories/lang/base.v
index 7c49f7d19d86339bf47577dedce435bb75d23b77..81336b430b88121309fbdfdba0c0522dbab5d746 100644
--- a/theories/lang/base.v
+++ b/theories/lang/base.v
@@ -250,6 +250,11 @@ Proof.
     end; auto.
 Qed.
 
+(* Lemmas we don't get for free because we are not an Iris language. *)
+Lemma as_val0_is_Some e :
+  (∃ v : base.val, base.of_val v = e) → is_Some (base.to_val e).
+Proof. intros [v <-]. rewrite base.to_of_val. eauto. Qed.
+
 (** Closed expressions *)
 Lemma is_closed_weaken X Y e : is_closed X e → X ⊆ Y → is_closed Y e.
 Proof. revert X Y; induction e; abstract naive_solver (eauto; set_solver). Qed.
diff --git a/theories/lifting.v b/theories/lifting.v
index a1a8d69a5638a38738aa30278d3e98d31b4e22ae..650dd0cb41254487fbf9cf0826c6695a24849027 100644
--- a/theories/lifting.v
+++ b/theories/lifting.v
@@ -38,7 +38,7 @@ Proof.
   edestruct (Hatomic σ1 e2 σ2 efs) as [v2 <-%of_to_val]; eauto.
   iDestruct ("H" $! v2 σ2 efs with "[$oP]") as ">[HΦ $]"; first by auto.
   iMod "Hclose". iMod "HΦ". iApply wp_value; eauto.
-  exact: to_of_val.
+  exact: of_to_val.
 Qed.
 
 Lemma wp_lift_atomic_head_step2 {E Φ} e1 σ1 :
@@ -945,12 +945,13 @@ Close Scope positive.
 End lifting.
 
 
-Local Ltac solve_exec_safe := intros; subst; do 3 eexists; do 2!econstructor; eauto.
+Local Ltac solve_exec_safe := intros; subst; do 3 eexists; do 2!econstructor; eauto using base.to_of_val.
 Local Ltac solve_exec_puredet := simpl; intros; inv_head_step.
 Local Ltac solve_pure_exec :=
-  unfold IntoVal, AsVal in *; subst;
-  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
-  apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
+  repeat match goal with H : IntoVal (_,_) (_,_) |- _ =>
+                   rewrite /IntoVal /= /of_val in H; revert H; intros [= ?] end;
+  repeat match goal with H : AsVal (_,_) |- _ => destruct H as [[??] [= ??]] end;
+  subst; apply det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
 Class AsRec (e : base.expr) (f x : base.binder) (erec : base.expr) :=
   as_rec : e = base.Rec f x erec.
@@ -963,25 +964,19 @@ Global Instance pure_rec f x (erec e1 e2 : base.expr) V
        `{!AsVal (e2,V), AsRec e1 f x erec, base.Closed (f :b: x :b: []) erec}:
   PureExec True (base.App e1 e2, V) (base.subst' x e2 (base.subst' f e1 erec), V).
 Proof.
-  intros. unfold AsRec in *.
-  move/fmap_is_Some: (AsVal0) => /= ?. solve_pure_exec. (* TODO: fix this *)
+  intros. unfold AsRec in *. solve_pure_exec.
 Qed.
 
 Global Instance pure_unop op e v v' V `{!IntoVal (e,V) (v,V)}:
   PureExec (base.un_op_eval op v = Some v') (base.UnOp op e, V) (base.of_val v', V).
 Proof.
-  intros.
-  move/fmap_Some: IntoVal0 => /= [? [? [->]]].
-  solve_pure_exec.
+  intros. solve_pure_exec.
 Qed.
 
 Global Instance pure_binop op e1 e2 v1 v2 v' V `{!IntoVal (e1,V) (v1,V), !IntoVal (e2,V) (v2,V)}:
   PureExec (base.bin_op_eval op v1 v2 = Some v') (base.BinOp op e1 e2, V) (base.of_val v',V).
 Proof.
-  intros.
-  move/fmap_Some: IntoVal0 => /= [? [? [->]]].
-  move/fmap_Some: IntoVal1 => /= [? [? [->]]].
-  solve_pure_exec.
+  intros. solve_pure_exec.
 Qed.
 
 Global Instance pure_if_true e1 e2:
diff --git a/theories/lifting_vProp.v b/theories/lifting_vProp.v
index 63dc2559f9d11562996036ef82d77ebe70139824..288af7c8ddd943dac168ce1d5d33d0dbe0672440 100644
--- a/theories/lifting_vProp.v
+++ b/theories/lifting_vProp.v
@@ -87,14 +87,14 @@ Global Instance AsRec_rec_locked_val v f x e :
 Proof. by unlock. Qed.
 
 
-Local Ltac solve_exec_safe := intros; subst; do 2 eexists; exists nil; do 2!econstructor; eauto.
+Local Ltac solve_exec_safe := intros; subst; do 2 eexists; exists nil; do 2!econstructor; eauto using base.to_of_val.
 Local Ltac solve_exec_puredet := simpl; intros; inv_head_step;
   repeat match goal with | [ X : View * state |- _ ] => destruct X end;
   match goal with | [ X : [] = map _ ?efs |- _ ] => destruct efs; [|discriminate] end;
   simpl in *; simplify_eq; done.
 Local Ltac solve_pure_exec :=
-  unfold IntoVal,AsVal,AsRec in *; subst;
-  repeat match goal with H : is_Some _ |- _ => destruct H as [??] end;
+  unfold IntoVal,AsRec in *; subst;
+  repeat match goal with H : AsVal _ |- _ => destruct H as [??] end;
   apply ectx_language.det_head_step_pure_exec; [ solve_exec_safe | solve_exec_puredet ].
 
 Global Instance pure_rec f x (erec e1 e2 : base.expr)
diff --git a/theories/tactics.v b/theories/tactics.v
index 017818b09d45d7f2b227ee4058f47f0c1b524068..aed8f26704522c8b7f242218fb8c704b71c2d8c2 100644
--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -145,28 +145,25 @@ Fixpoint to_val0 (e : expr0) : option base.val :=
 Definition to_val (e : expr) : option val :=
   (λ v0, (v0, e.2)) <$> to_val0 (e.1).
 Lemma to_val0_Some e v :
-  to_val0 e = Some v → base.to_val (to_expr' e) = Some v.
+  to_val0 e = Some v → base.of_val v = to_expr' e.
 Proof.
-  revert v. induction e; intros; simplify_option_eq; rewrite ?to_of_val; auto.
-  - by rewrite base.to_of_val.
-  - do 2 f_equal. apply proof_irrel.
-  - exfalso. unfold base.Closed in *; eauto using is_closed_correct0.
+  revert v. induction e; intros; simplify_option_eq; try f_equal; auto using of_to_val.
 Qed.
 Lemma to_val_Some e v :
-  to_val e = Some v → ra_lang.to_val (to_expr e) = Some v.
+  to_val e = Some v → ra_lang.of_val v = to_expr e.
 Proof.
-  destruct e, v. cbv -[to_val0 base.to_val to_expr'].
-  case H: (to_val0 e) => //.
-  erewrite to_val0_Some; by eauto.
+  destruct e, v. cbv -[to_val0 base.of_val to_expr'].
+  case H: (to_val0 e) =>? //.
+  erewrite <-to_val0_Some; try simplify_eq; eauto.
 Qed.
 
 Lemma to_val0_is_Some e :
-  is_Some (to_val0 e) → is_Some (base.to_val (to_expr' e)).
+  is_Some (to_val0 e) → ∃ v, base.of_val v = to_expr' e.
 Proof. intros [v ?]; exists v; eauto using to_val0_Some. Qed.
 
 Lemma to_val_is_Some e :
-  is_Some (to_val e) → is_Some (ra_lang.to_val (to_expr e)).
-Proof. move/fmap_is_Some => H. apply/fmap_is_Some. exact: to_val0_is_Some. Qed.
+  is_Some (to_val e) → ∃ v, ra_lang.of_val v = to_expr e.
+Proof. intros [v ?]; exists v; eauto using to_val_Some. Qed.
 
 Fixpoint subst0 (x : string) (es : expr0) (e : expr0)  : expr0 :=
   match e with
@@ -238,7 +235,7 @@ Proof.
     { intros [v Hv]. eexists. unfold ra_lang.to_val. simpl. rewrite Hv //. }
     clear dependent π π'.
     destruct e=> //; destruct Ki; repeat (simplify_eq/=; case_match=>//);
-      naive_solver eauto using to_val0_is_Some.
+      try naive_solver eauto using as_val0_is_Some, to_val0_is_Some.
 Qed.
 End W.
 
@@ -293,10 +290,10 @@ Ltac solve_to_val :=
 Ltac solve_into_val :=
   match goal with
   | |- IntoVal (?e,?V) (?v,?V) =>
-     let e' := W.of_expr0 e in change ((to_val (W.to_expr0 e',V)) = Some (v,V));
+     let e' := W.of_expr0 e in change (ra_lang.of_val (v,V) = (W.to_expr0 e',V));
      apply W.to_val_Some; simpl; unfold W.to_expr; reflexivity
   | |- IntoVal (?e) (?v) =>
-     let e' := W.of_expr0 e in change ((base.to_val (W.to_expr' e')) = Some (v));
+     let e' := W.of_expr0 e in change (base.of_val v = W.to_expr' e');
      apply W.to_val0_Some; simpl; unfold W.to_expr0; reflexivity
   end.
 Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
@@ -304,10 +301,10 @@ Hint Extern 10 (IntoVal _ _) => solve_into_val : typeclass_instances.
 Ltac solve_as_val :=
   match goal with
   | |- AsVal (?e,?V) =>
-     let e' := W.of_expr0 e in change (is_Some (to_val (W.to_expr (e',V))));
+     let e' := W.of_expr0 e in change (∃ v, ra_lang.of_val (v,  V) = W.to_expr (e',V));
      apply W.to_val_is_Some, (bool_decide_unpack _); vm_compute; exact I
   | |- AsVal (?e) =>
-     let e' := W.of_expr0 e in change (is_Some (base.to_val (W.to_expr' e')));
+     let e' := W.of_expr0 e in change (∃ v, base.of_val v = W.to_expr' e');
      apply W.to_val0_is_Some, (bool_decide_unpack _); vm_compute; exact I
   end.
 Hint Extern 10 (AsVal _) => solve_as_val : typeclass_instances.
diff --git a/theories/wp_tactics_vProp.v b/theories/wp_tactics_vProp.v
index 5d0640c7a64542fcc9b90fbdc3c9ad9e5b1c42e2..8a7fb72fdcecd80c11b051107e07f0f9c2846087 100644
--- a/theories/wp_tactics_vProp.v
+++ b/theories/wp_tactics_vProp.v
@@ -30,7 +30,7 @@ Qed.
 Lemma tac_wp_value `{foundationG Σ} Δ E Φ e v :
   (IntoVal (e) (v)) →
   envs_entails Δ (Φ v) → envs_entails Δ (WP e @ E {{ Φ }}).
-Proof. rewrite envs_entails_eq=> IV ->. now apply: wp_value. Qed.
+Proof. rewrite envs_entails_eq=> <- ->. now apply: wp_value'. Qed.
 
 Ltac wp_value_head := eapply tac_wp_value; [apply _|lazy beta].