diff --git a/ProofMode.md b/ProofMode.md
index 0ca7b0b55af7098f71f2f8235464f1b115295aff..f7018ae66e2909688a05489f10ed3f7c1e8529e0 100644
--- a/ProofMode.md
+++ b/ProofMode.md
@@ -202,6 +202,7 @@ _introduction patterns_:
 - `[ipat1|ipat2]` : disjunction elimination.
 - `[]` : false elimination.
 - `%` : move the hypothesis to the pure Coq context (anonymously).
+- `->` and `<-` : rewrite using a pure Coq equality
 - `# ipat` : move the hypothesis to the persistent context.
 - `> ipat` : eliminate a modality (if the goal permits).
 
diff --git a/theories/proofmode/intro_patterns.v b/theories/proofmode/intro_patterns.v
index 7d1c308a4d5cb15c612fc21f1ee40456a218ff43..ed608c6455dbaf166e40d1be74989ff8c4d682d0 100644
--- a/theories/proofmode/intro_patterns.v
+++ b/theories/proofmode/intro_patterns.v
@@ -11,6 +11,7 @@ Inductive intro_pat :=
   | IPureElim : intro_pat
   | IAlwaysElim : intro_pat → intro_pat
   | IModalElim : intro_pat → intro_pat
+  | IRewrite : direction → intro_pat (* true = ->, false = <- *)
   | IPureIntro : intro_pat
   | IAlwaysIntro : intro_pat
   | IModalIntro : intro_pat
@@ -84,6 +85,7 @@ Fixpoint parse_go (ts : list token) (k : stack) : option stack :=
   | TPure :: ts => parse_go ts (SPat IPureElim :: k)
   | TAlways :: ts => parse_go ts (SAlwaysElim :: k)
   | TModal :: ts => parse_go ts (SModalElim :: k)
+  | TArrow d :: ts => parse_go ts (SPat (IRewrite d) :: k)
   | TPureIntro :: ts => parse_go ts (SPat IPureIntro :: k)
   | TAlwaysIntro :: ts => parse_go ts (SPat IAlwaysIntro :: k)
   | TModalIntro :: ts => parse_go ts (SPat IModalIntro :: k)
diff --git a/theories/proofmode/tactics.v b/theories/proofmode/tactics.v
index 6164ad82eb2274ba0c426e24d736bc84b80ba033..cfd64347b9cd42d583610d2a6320c78052d14952 100644
--- a/theories/proofmode/tactics.v
+++ b/theories/proofmode/tactics.v
@@ -854,6 +854,8 @@ Local Tactic Notation "iDestructHyp" constr(H) "as" constr(pat) :=
        let Hy := iFresh in iAndDestruct Hz as Hz Hy; go Hz pat1; go Hy pat2
     | IList [[?pat1];[?pat2]] => iOrDestruct Hz as Hz Hz; [go Hz pat1|go Hz pat2]
     | IPureElim => iPure Hz as ?
+    | IRewrite tokens.Right => iPure Hz as ->
+    | IRewrite tokens.Left => iPure Hz as <-
     | IAlwaysElim ?pat => iPersistent Hz; go Hz pat
     | IModalElim ?pat => iModCore Hz; go Hz pat
     | _ => fail "iDestruct:" pat "invalid"
diff --git a/theories/proofmode/tokens.v b/theories/proofmode/tokens.v
index c45c14862fc2328289f7a16bc26c7f0d49b2676d..a94611fa1de3ab7e9f9dc6bd2a207e9c8d170890 100644
--- a/theories/proofmode/tokens.v
+++ b/theories/proofmode/tokens.v
@@ -1,6 +1,9 @@
 From stdpp Require Export strings.
 Set Default Proof Using "Type".
 
+(* TODO: Move elsewhere *)
+Inductive direction := Left | Right.
+
 Inductive token :=
   | TName : string → token
   | TNat : nat → token
@@ -25,7 +28,8 @@ Inductive token :=
   | TForall : token
   | TAll : token
   | TMinus : token
-  | TSep : token.
+  | TSep : token
+  | TArrow : direction → token.
 
 Inductive state :=
   | SName : string → state
@@ -64,6 +68,8 @@ Fixpoint tokenize_go (s : string) (k : list token) (kn : state) : list token :=
   | String "/" (String "=" s) => tokenize_go s (TSimpl :: cons_state kn k) SNone
   | String "*" (String "*" s) => tokenize_go s (TAll :: cons_state kn k) SNone
   | String "*" s => tokenize_go s (TForall :: cons_state kn k) SNone
+  | String "-" (String ">" s) => tokenize_go s (TArrow Right :: cons_state kn k) SNone
+  | String "<" (String "-" s) => tokenize_go s (TArrow Left :: cons_state kn k) SNone
   | String "-" s => tokenize_go s (TMinus :: cons_state kn k) SNone
   | String (Ascii.Ascii false true false false false true true true) (* unicode ∗ *)
       (String (Ascii.Ascii false false false true false false false true)
diff --git a/theories/tests/proofmode.v b/theories/tests/proofmode.v
index 71505deab13254b7af0dbea0c04a4133b18e39a7..1ed83a72fee986a25e3bb839fa527b01660ebeff 100644
--- a/theories/tests/proofmode.v
+++ b/theories/tests/proofmode.v
@@ -229,6 +229,10 @@ Proof.
   iIntros "* **". (* Test that fast intros do not work under modalities *)
   iIntros ([]).
 Qed.
+
+Lemma test_iIntros_rewrite P (x1 x2 x3 x4 : nat) :
+  x1 = x2 → (⌜ x2 = x3 ⌝ ∗ ⌜ x3 ≡ x4 ⌝ ∗ P) -∗ ⌜ x1 = x4 ⌝ ∗ P.
+Proof. iIntros (?) "(-> & -> & $)"; auto. Qed.
 End tests.
 
 Section more_tests.