diff --git a/CHANGELOG.md b/CHANGELOG.md
index 10ed7959b0bee06177b33ff05e287f3ddae229b5..8f5b09bab19f9c3629b8f2f4ee6a230294b4c433 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -85,6 +85,8 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
   of evars, which often led to divergence. There are a few places where type
   annotations are now needed.
 * Move the `prelude` folder to its own project: std++
+* The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
+  stated in the logic, i.e. they are `iApply` friendly.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
diff --git a/theories/base_logic/derived.v b/theories/base_logic/derived.v
index 76e2f0b93f95fe2009df2061b39f9c2611ef8971..c0324fc45eab0d3101490e26d99126bf90f149a3 100644
--- a/theories/base_logic/derived.v
+++ b/theories/base_logic/derived.v
@@ -298,13 +298,19 @@ Hint Resolve internal_eq_refl'.
 Lemma equiv_internal_eq {A : ofeT} P (a b : A) : a ≡ b → P ⊢ a ≡ b.
 Proof. by intros ->. Qed.
 Lemma internal_eq_sym {A : ofeT} (a b : A) : a ≡ b ⊢ b ≡ a.
-Proof. apply (internal_eq_rewrite a b (λ b, b ≡ a)%I); auto. solve_proper. Qed.
-Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : Contractive Ψ} : (P ⊢ ▷ (a ≡ b)) → (P ⊢ Ψ a) → P ⊢ Ψ b.
 Proof.
-  move: HΨ=> /contractiveI HΨ Heq ?.
-  apply (internal_eq_rewrite (Ψ a) (Ψ b) id _)=>//=. by rewrite -HΨ.
+  rewrite (internal_eq_rewrite a b (λ b, b ≡ a)%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl True_impl.
 Qed.
+Lemma f_equiv {A B : ofeT} (f : A → B) `{!NonExpansive f} x y :
+  x ≡ y ⊢ f x ≡ f y.
+Proof.
+  rewrite (internal_eq_rewrite x y (λ y, f x ≡ f y)%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl True_impl.
+Qed.
+Lemma internal_eq_rewrite_contractive {A : ofeT} a b (Ψ : A → uPred M)
+  {HΨ : Contractive Ψ} : ▷ (a ≡ b) ⊢ Ψ a → Ψ b.
+Proof. move: HΨ=> /contractiveI ->. by rewrite (internal_eq_rewrite _ _ id). Qed.
 
 Lemma pure_impl_forall φ P : (⌜φ⌝ → P) ⊣⊢ (∀ _ : φ, P).
 Proof.
@@ -345,8 +351,8 @@ Lemma equiv_iff P Q : (P ⊣⊢ Q) → (P ↔ Q)%I.
 Proof. intros ->; apply iff_refl. Qed.
 Lemma internal_eq_iff P Q : P ≡ Q ⊢ P ↔ Q.
 Proof.
-  apply (internal_eq_rewrite P Q (λ Q, P ↔ Q))%I;
-    first solve_proper; auto using iff_refl.
+  rewrite (internal_eq_rewrite P Q (λ Q, P ↔ Q)%I ltac:(solve_proper)).
+  by rewrite -(iff_refl True) True_impl.
 Qed.
 
 (* Derived BI Stuff *)
@@ -531,9 +537,8 @@ Qed.
 Lemma plainly_internal_eq {A:ofeT} (a b : A) : ■ (a ≡ b) ⊣⊢ a ≡ b.
 Proof.
   apply (anti_symm (⊢)); auto using persistently_elim.
-  apply (internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I); auto.
-  { intros n; solve_proper. }
-  rewrite -(internal_eq_refl a) plainly_pure; auto.
+  rewrite {1}(internal_eq_rewrite a b (λ b, ■ (a ≡ b))%I ltac:(solve_proper)).
+  by rewrite -internal_eq_refl plainly_pure True_impl.
 Qed.
 
 Lemma plainly_and_sep_l_1 P Q : ■ P ∧ Q ⊢ ■ P ∗ Q.
@@ -946,8 +951,8 @@ Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a).
 Proof.
   intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
   rewrite (timelessP (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and.
-  apply except_0_mono. rewrite internal_eq_sym.
-  apply (internal_eq_rewrite b a (uPred_ownM)); first apply _; auto.
+  apply except_0_mono. rewrite internal_eq_sym. apply impl_elim_r'.
+  apply: internal_eq_rewrite.
 Qed.
 Global Instance from_option_timeless {A} P (Ψ : A → uPred M) (mx : option A) :
   (∀ x, Timeless (Ψ x)) → Timeless P → Timeless (from_option Ψ P mx).
diff --git a/theories/base_logic/lib/boxes.v b/theories/base_logic/lib/boxes.v
index 3d7a7ca77bfdd5f43e0ea1773ea9591f52e73bda..cf8aff8a07e1225775e73eab7983b4532044d26f 100644
--- a/theories/base_logic/lib/boxes.v
+++ b/theories/base_logic/lib/boxes.v
@@ -273,7 +273,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 true). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
   - iMod (slice_delete_empty with "Hslice Hbox") as (P') "[Heq Hbox]"; try done.
     iMod (slice_insert_empty with "Hbox") as (γ1 ?) "[#Hslice1 Hbox]".
@@ -281,7 +281,7 @@ Proof.
     iExists γ1, γ2. iIntros "{$% $#} !>". iSplit; last iSplit; try iPureIntro.
     { by eapply lookup_insert_None. }
     { by apply (lookup_insert_None (delete γ f) γ1 γ2 false). }
-    iNext. eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iNext. iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq". iPureIntro. by rewrite assoc (comm _ Q2).
 Qed.
 
@@ -298,14 +298,14 @@ Proof.
     iMod (slice_insert_full _ _ _ _ (Q1 ∗ Q2)%I with "[$HQ1 $HQ2] Hbox")
       as (γ ?) "[#Hslice Hbox]"; first done.
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
   - iMod (slice_delete_empty with "Hslice1 Hbox") as (P1) "(Heq1 & Hbox)"; try done.
     iMod (slice_delete_empty with "Hslice2 Hbox") as (P2) "(Heq2 & Hbox)"; first done.
     { by simplify_map_eq. }
     iMod (slice_insert_empty with "Hbox") as (γ ?) "[#Hslice Hbox]".
     iExists γ. iIntros "{$% $#} !>". iNext.
-    eapply internal_eq_rewrite_contractive; [by apply _| |by eauto].
+    iApply (internal_eq_rewrite_contractive with "[#] Hbox").
     iNext. iRewrite "Heq1". iRewrite "Heq2". by rewrite assoc.
 Qed.
 End box.
diff --git a/theories/base_logic/lib/iprop.v b/theories/base_logic/lib/iprop.v
index b0462acf5e89fbc7a224c260f94be3770b7dc2ae..a36fb468200f92a5b9abfa9d628d918c11f7f548 100644
--- a/theories/base_logic/lib/iprop.v
+++ b/theories/base_logic/lib/iprop.v
@@ -152,6 +152,5 @@ Lemma iProp_unfold_equivI {Σ} (P Q : iProp Σ) :
   iProp_unfold P ≡ iProp_unfold Q ⊢ (P ≡ Q : iProp Σ).
 Proof.
   rewrite -{2}(iProp_fold_unfold P) -{2}(iProp_fold_unfold Q).
-  eapply (uPred.internal_eq_rewrite _ _ (λ z,
-    iProp_fold (iProp_unfold P) ≡ iProp_fold z))%I; auto with I; solve_proper.
+  apply: uPred.f_equiv.
 Qed.
diff --git a/theories/base_logic/lib/saved_prop.v b/theories/base_logic/lib/saved_prop.v
index 4ce4a3ce2da7b3035353289cb0f9c695387c628c..2ff8cc19d2601f5d6ac72a4c08069d520a1bfba9 100644
--- a/theories/base_logic/lib/saved_prop.v
+++ b/theories/base_logic/lib/saved_prop.v
@@ -43,8 +43,6 @@ Section saved_prop.
     assert (∀ z, G2 (G1 z) ≡ z) as help.
     { intros z. rewrite /G1 /G2 -cFunctor_compose -{2}[z]cFunctor_id.
       apply (ne_proper (cFunctor_map F)); split=>?; apply iProp_fold_unfold. }
-    rewrite -{2}[x]help -{2}[y]help. apply later_mono.
-    apply (internal_eq_rewrite (G1 x) (G1 y) (λ z, G2 (G1 x) ≡ G2 z))%I;
-      first solve_proper; auto with I.
+    rewrite -{2}[x]help -{2}[y]help. apply later_mono, f_equiv, _.
   Qed.
 End saved_prop.
diff --git a/theories/base_logic/primitive.v b/theories/base_logic/primitive.v
index f251fbb1a1c7fc350c8c38497e537f418a0cf9b4..3aab1eeb26c85419f51946db655848aa2e04a47a 100644
--- a/theories/base_logic/primitive.v
+++ b/theories/base_logic/primitive.v
@@ -395,13 +395,9 @@ Proof. unseal; intros HΦΨ; split=> n x ? [a ?]; by apply HΦΨ with a. Qed.
 
 Lemma internal_eq_refl {A : ofeT} (a : A) : uPred_valid (M:=M) (a ≡ a).
 Proof. unseal; by split=> n x ??; simpl. Qed.
-Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) P
-  {HΨ : NonExpansive Ψ} : (P ⊢ a ≡ b) → (P ⊢ Ψ a) → P ⊢ Ψ b.
-Proof.
-  unseal; intros Hab Ha; split=> n x ??. apply HΨ with n a; auto.
-  - by symmetry; apply Hab with x.
-  - by apply Ha.
-Qed.
+Lemma internal_eq_rewrite {A : ofeT} a b (Ψ : A → uPred M) :
+  NonExpansive Ψ → a ≡ b ⊢ Ψ a → Ψ b.
+Proof. intros HΨ. unseal; split=> n x ?? n' x' ??? Ha. by apply HΨ with n a. Qed.
 
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : (P ⊢ Q) → (P' ⊢ Q') → P ∗ P' ⊢ Q ∗ Q'.
diff --git a/theories/proofmode/coq_tactics.v b/theories/proofmode/coq_tactics.v
index 9ef43f8d7271b5157c178faddc766ec2e5c77abb..138b5c473835d65cdb6d3355cb3e9ce53dcb905d 100644
--- a/theories/proofmode/coq_tactics.v
+++ b/theories/proofmode/coq_tactics.v
@@ -770,12 +770,14 @@ Lemma tac_rewrite Δ i p Pxy d Q :
   ∀ {A : ofeT} (x y : A) (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (Q ⊣⊢ Φ (if d is Left then y else x)) →
-    (NonExpansive Φ) →
+    NonExpansive Φ →
     (Δ ⊢ Φ (if d is Left then x else y)) → Δ ⊢ Q.
 Proof.
-  intros ? A x y ? HPxy -> ?; apply internal_eq_rewrite; auto.
-  rewrite {1}envs_lookup_sound' //; rewrite sep_elim_l HPxy.
-  destruct d; auto using internal_eq_sym.
+  intros ? A x y Φ HPxy -> ? HΔ.
+  rewrite -(idemp (∧)%I (of_envs Δ)) {1}envs_lookup_sound' //.
+  rewrite sep_elim_l HPxy HΔ. apply impl_elim_l'. destruct d.
+  - by apply internal_eq_rewrite.
+  - rewrite internal_eq_sym. by apply internal_eq_rewrite.
 Qed.
 
 Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
@@ -784,20 +786,19 @@ Lemma tac_rewrite_in Δ i p Pxy j q P d Q :
   ∀ {A : ofeT} Δ' x y (Φ : A → uPred M),
     (Pxy ⊢ x ≡ y) →
     (P ⊣⊢ Φ (if d is Left then y else x)) →
-    (NonExpansive Φ) →
+    NonExpansive Φ →
     envs_simple_replace j q (Esnoc Enil j (Φ (if d is Left then x else y))) Δ = Some Δ' →
     (Δ' ⊢ Q) → Δ ⊢ Q.
 Proof.
   intros ?? A Δ' x y Φ HPxy HP ?? <-.
-  rewrite -(idemp uPred_and Δ) {2}(envs_lookup_sound' _ i) //.
+  rewrite -(idemp uPred_and (of_envs Δ)) {2}(envs_lookup_sound' _ i) //.
   rewrite sep_elim_l HPxy and_sep_r.
   rewrite (envs_simple_replace_sound _ _ j) //; simpl.
-  rewrite HP right_id -assoc; apply wand_elim_r'. destruct d.
-  - apply (internal_eq_rewrite x y (λ y, □?q Φ y -∗ Δ')%I);
-      eauto with I. solve_proper.
-  - apply (internal_eq_rewrite y x (λ y, □?q Φ y -∗ Δ')%I);
-      eauto using internal_eq_sym with I.
-    solve_proper.
+  rewrite HP right_id -assoc (sep_and _ (_ ≡ _)).
+  apply wand_elim_r', impl_elim_r'. destruct d.
+  - apply (internal_eq_rewrite _ _ (λ y, □?q Φ y -∗ _)%I). solve_proper.
+  - rewrite internal_eq_sym.
+    apply (internal_eq_rewrite _ _ (λ y, □?q Φ y -∗ _)%I). solve_proper.
 Qed.
 
 (** * Conjunction splitting *)