diff --git a/proofmode/class_instances.v b/proofmode/class_instances.v
index 7c3f504f2e029b66b651df82bc1b860768ae1e2c..988f337544dccec7128349279b1a7fc6eb0587a5 100644
--- a/proofmode/class_instances.v
+++ b/proofmode/class_instances.v
@@ -327,11 +327,21 @@ Global Instance into_exist_always {A} P (Φ : A → uPred M) :
   IntoExist P Φ → IntoExist (□ P) (λ a, □ (Φ a))%I.
 Proof. rewrite /IntoExist=> HP. by rewrite HP always_exist. Qed.
 
-(* IsTrueNow *)
+(* IntoNowTrue *)
+Global Instance into_now_True_now_True P : IntoNowTrue (â—‡ P) P.
+Proof. done. Qed.
+Global Instance into_now_True_timeless P : TimelessP P → IntoNowTrue (▷ P) P.
+Proof. done. Qed.
+
+(* IsNowTrue *)
 Global Instance is_now_True_now_True P : IsNowTrue (â—‡ P).
 Proof. by rewrite /IsNowTrue now_True_idemp. Qed.
 Global Instance is_now_True_later P : IsNowTrue (â–· P).
 Proof. by rewrite /IsNowTrue now_True_later. Qed.
+Global Instance is_now_True_rvs P : IsNowTrue P → IsNowTrue (|=r=> P).
+Proof.
+  rewrite /IsNowTrue=> HP. by rewrite -{2}HP -now_True_rvs -(now_True_intro P).
+Qed.
 
 (* FromViewShift *)
 Global Instance from_vs_rvs P : FromVs (|=r=> P) P.
diff --git a/proofmode/classes.v b/proofmode/classes.v
index 037de8467d3b37024c44225c83ad628925beb476..730e5ee773cd20e1a2e4a6bd843a1d8bac2fac90 100644
--- a/proofmode/classes.v
+++ b/proofmode/classes.v
@@ -55,6 +55,9 @@ Class IntoExist {A} (P : uPred M) (Φ : A → uPred M) :=
   into_exist : P ⊢ ∃ x, Φ x.
 Global Arguments into_exist {_} _ _ {_}.
 
+Class IntoNowTrue (P Q : uPred M) := into_now_True : P ⊢ ◇ Q.
+Global Arguments into_now_True : clear implicits.
+
 Class IsNowTrue (Q : uPred M) := is_now_True : ◇ Q ⊢ Q.
 Global Arguments is_now_True : clear implicits.
 
diff --git a/proofmode/coq_tactics.v b/proofmode/coq_tactics.v
index 1c0d4f3ac4d9c2452260434c35f52d52232059bf..83dd251a310a3172a4641051cefb0eb21b2689a2 100644
--- a/proofmode/coq_tactics.v
+++ b/proofmode/coq_tactics.v
@@ -375,15 +375,15 @@ Proof.
   by rewrite right_id always_and_sep_l' wand_elim_r HQ.
 Qed.
 
-Lemma tac_timeless Δ Δ' i p P Q :
+Lemma tac_timeless Δ Δ' i p P P' Q :
   IsNowTrue Q →
-  envs_lookup i Δ = Some (p, ▷ P)%I → TimelessP P →
-  envs_simple_replace i p (Esnoc Enil i P) Δ = Some Δ' →
+  envs_lookup i Δ = Some (p, P) → IntoNowTrue P P' →
+  envs_simple_replace i p (Esnoc Enil i P') Δ = Some Δ' →
   (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ???? HQ. rewrite envs_simple_replace_sound //; simpl.
-  rewrite always_if_later right_id HQ -{2}(is_now_True Q).
-  by rewrite (timelessP (â–¡?p P)) now_True_frame_r wand_elim_r.
+  rewrite right_id HQ -{2}(is_now_True Q).
+  by rewrite (into_now_True P) -now_True_always_if now_True_frame_r wand_elim_r.
 Qed.
 
 (** * Always *)
diff --git a/proofmode/tactics.v b/proofmode/tactics.v
index dcf66b391b5f1d69ed2c6a81e789f9b470328b0b..85791ec2176013fee96e509a2a6545dd209db0b0 100644
--- a/proofmode/tactics.v
+++ b/proofmode/tactics.v
@@ -496,11 +496,11 @@ Tactic Notation "iNext":=
      apply _ || fail "iNext:" P "does not contain laters"|].
 
 Tactic Notation "iTimeless" constr(H) :=
-  eapply tac_timeless with _ H _ _;
+  eapply tac_timeless with _ H _ _ _;
     [let Q := match goal with |- IsNowTrue ?Q => Q end in
      apply _ || fail "iTimeless: cannot remove later of timeless hypothesis in goal" Q
     |env_cbv; reflexivity || fail "iTimeless:" H "not found"
-    |let P := match goal with |- TimelessP ?P => P end in
+    |let P := match goal with |- IntoNowTrue ?P _ => P end in
      apply _ || fail "iTimeless:" P "not timeless"
     |env_cbv; reflexivity|].