diff --git a/CHANGELOG.md b/CHANGELOG.md
index afbae91b4ec092b6d9191dc1ad3edcfef9dca12c..a1b9a8f564b1985c058ac61a135ddd74a08f2afe 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -5,6 +5,9 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 
 ## Iris 3.0
 
+# Lifting lemmas do no longer take as hypothesis the fact the the
+  considered expression is not a value. This is deduced from the fact that
+  it is reducible.
 * View shifts are radically simplified to just internalize frame-preserving
   updates.  Weakestpre is defined inside the logic, and invariants and view
   shifts with masks are also coded up inside Iris.  Adequacy of weakestpre
diff --git a/heap_lang/lifting.v b/heap_lang/lifting.v
index 917c0002535885440ee3463fcbb9b946834e9340..7767e5ecff41f81d65068d538d52f9b3ee2864e7 100644
--- a/heap_lang/lifting.v
+++ b/heap_lang/lifting.v
@@ -61,8 +61,8 @@ Lemma wp_load_pst E σ l v Φ :
   σ !! l = Some v →
   ▷ ownP σ ★ ▷ (ownP σ ={E}=★ Φ v) ⊢ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
 Proof.
-  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto 10.
-  intros; inv_head_step; eauto 10.
+  intros. rewrite -(wp_lift_atomic_det_head_step' σ v σ); eauto.
+  intros; inv_head_step; eauto.
 Qed.
 
 Lemma wp_store_pst E σ l v v' Φ :
@@ -89,7 +89,7 @@ Lemma wp_cas_suc_pst E σ l v1 v2 Φ :
   ⊢ WP CAS (Lit (LitLoc l)) (of_val v1) (of_val v2) @ E {{ Φ }}.
 Proof.
   intros. rewrite -(wp_lift_atomic_det_head_step' σ (LitV $ LitBool true)
-    (<[l:=v2]>σ)); eauto 10.
+    (<[l:=v2]>σ)); eauto.
   intros; inv_head_step; eauto.
 Qed.
 
diff --git a/program_logic/ectx_lifting.v b/program_logic/ectx_lifting.v
index 7d329558b564a425bb82efff655babbb2abcf7d1..f0361cfa4c7c1c34f22ed26267c9c37c687804dc 100644
--- a/program_logic/ectx_lifting.v
+++ b/program_logic/ectx_lifting.v
@@ -5,7 +5,7 @@ From iris.proofmode Require Import tactics.
 
 Section wp.
 Context {expr val ectx state} {Λ : EctxLanguage expr val ectx state}.
-Context `{irisG (ectx_lang expr) Σ}.
+Context `{irisG (ectx_lang expr) Σ} `{Inhabited state}.
 Implicit Types P : iProp Σ.
 Implicit Types Φ : val → iProp Σ.
 Implicit Types v : val.
@@ -17,27 +17,25 @@ Lemma wp_ectx_bind {E e} K Φ :
 Proof. apply: weakestpre.wp_bind. Qed.
 
 Lemma wp_lift_head_step E Φ e1 :
-  to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ head_reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ head_step e1 σ1 e2 σ2 efs ★ ownP σ2
           ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "H". iApply (wp_lift_step E); try done.
+  iIntros "H". iApply (wp_lift_step E); try done.
   iVs "H" as (σ1) "(%&Hσ1&Hwp)". iVsIntro. iExists σ1.
   iSplit; first by eauto. iFrame. iNext. iIntros (e2 σ2 efs) "[% ?]".
   iApply "Hwp". by eauto.
 Qed.
 
 Lemma wp_lift_pure_head_step E Φ e1 :
-  to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, head_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (▷ ∀ e2 efs σ, ■ head_step e1 σ e2 σ efs →
     WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (???) "H". iApply wp_lift_pure_step; eauto. iNext.
+  iIntros (??) "H". iApply wp_lift_pure_step; eauto. iNext.
   iIntros (????). iApply "H". eauto.
 Qed.
 
@@ -75,7 +73,6 @@ Proof.
 Qed.
 
 Lemma wp_lift_pure_det_head_step {E Φ} e1 e2 efs :
-  to_val e1 = None →
   (∀ σ1, head_reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', head_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs') →
   ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
diff --git a/program_logic/lifting.v b/program_logic/lifting.v
index b5f27323774c53dcee77174dd8fcf9f81f5172db..e1dd6e66995336ed3e90cae049635e1300cc657e 100644
--- a/program_logic/lifting.v
+++ b/program_logic/lifting.v
@@ -12,29 +12,32 @@ Implicit Types P Q : iProp Σ.
 Implicit Types Φ : val Λ → iProp Σ.
 
 Lemma wp_lift_step E Φ e1 :
-  to_val e1 = None →
   (|={E,∅}=> ∃ σ1, ■ reducible e1 σ1 ★ ▷ ownP σ1 ★
     ▷ ∀ e2 σ2 efs, ■ prim_step e1 σ1 e2 σ2 efs ★ ownP σ2
           ={∅,E}=★ WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
-  iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
-  iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
-  iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
-  iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
-  iApply "H"; eauto.
+  iIntros "H". rewrite wp_unfold /wp_pre.
+  destruct (to_val e1) as [v|] eqn:EQe1.
+  - iLeft. iExists v. iSplit. done. iVs "H" as (σ1) "[% _]".
+    by erewrite reducible_not_val in EQe1.
+  - iRight; iSplit; eauto.
+    iIntros (σ1) "Hσ". iVs "H" as (σ1') "(% & >Hσf & H)".
+    iDestruct (ownP_agree σ1 σ1' with "[-]") as %<-; first by iFrame.
+    iVsIntro; iSplit; [done|]; iNext; iIntros (e2 σ2 efs Hstep).
+    iVs (ownP_update σ1 σ2 with "[-H]") as "[$ ?]"; first by iFrame.
+    iApply "H"; eauto.
 Qed.
 
-Lemma wp_lift_pure_step E Φ e1 :
-  to_val e1 = None →
+Lemma wp_lift_pure_step `{Inhabited (state Λ)} E Φ e1 :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (▷ ∀ e2 efs σ, ■ prim_step e1 σ e2 σ efs →
     WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (He Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
+  iIntros (Hsafe Hstep) "H". rewrite wp_unfold /wp_pre; iRight; iSplit; auto.
+  { iPureIntro. eapply reducible_not_val, (Hsafe inhabitant). }
   iIntros (σ1) "Hσ". iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iSplit; [done|]; iNext; iIntros (e2 σ2 efs ?).
   destruct (Hstep σ1 e2 σ2 efs); auto; subst.
@@ -49,8 +52,7 @@ Lemma wp_lift_atomic_step {E Φ} e1 σ1 :
     (|={E}=> Φ v2) ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (Hatomic ?) "[Hσ H]".
-  iApply (wp_lift_step E _ e1); eauto using reducible_not_val.
+  iIntros (Hatomic ?) "[Hσ H]". iApply (wp_lift_step E _ e1).
   iApply pvs_intro'; [set_solver|iIntros "Hclose"].
   iExists σ1. iFrame "Hσ"; iSplit; eauto.
   iNext; iIntros (e2 σ2 efs) "[% Hσ]".
@@ -73,14 +75,13 @@ Proof.
   edestruct Hdet as (->&->%of_to_val%(inj of_val)&->). done. by iApply "Hσ2".
 Qed.
 
-Lemma wp_lift_pure_det_step {E Φ} e1 e2 efs :
-  to_val e1 = None →
+Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {E Φ} e1 e2 efs :
   (∀ σ1, reducible e1 σ1) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   ▷ (WP e2 @ E {{ Φ }} ★ [★ list] ef ∈ efs, WP ef {{ _, True }})
   ⊢ WP e1 @ E {{ Φ }}.
 Proof.
-  iIntros (?? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
+  iIntros (? Hpuredet) "?". iApply (wp_lift_pure_step E); try done.
   by intros; eapply Hpuredet. iNext. by iIntros (e' efs' σ (_&->&->)%Hpuredet).
 Qed.
 End lifting.