diff --git a/CHANGELOG.md b/CHANGELOG.md
index 10d4c4f02d99154a41ee86d2dfb16453ae62f5cd..09cab0b53989626127684da09a02515bd6855f3e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -63,6 +63,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   To make this work we also had to rename `inv_acc` -> `inv_alter`.
   (Most developments should be unaffected as the typical way to invoke these
   lemmas is through `iInv`, and that does not change.)
+* Added a construction `bi_rtc` to create reflexive transitive closures of
+  PROP-level binary relations.
 
 ## Iris 3.2.0 (released 2019-08-29)
 
diff --git a/_CoqProject b/_CoqProject
index 6afe26a4c84cc86d20bacea337a0880e996ec814..c6951c4fea17b376dbc955a6fa06ac76e7d26a86 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -63,6 +63,7 @@ theories/bi/lib/fractional.v
 theories/bi/lib/laterable.v
 theories/bi/lib/atomic.v
 theories/bi/lib/core.v
+theories/bi/lib/relations.v
 theories/base_logic/upred.v
 theories/base_logic/bi.v
 theories/base_logic/derived.v
diff --git a/theories/bi/lib/relations.v b/theories/bi/lib/relations.v
new file mode 100644
index 0000000000000000000000000000000000000000..fcea297c979ddf433dbeaee2e673af448b51baa7
--- /dev/null
+++ b/theories/bi/lib/relations.v
@@ -0,0 +1,95 @@
+(** This file provides a construction to lift a PROP-level binary relation to
+its reflexive transitive closure. *)
+From iris.bi.lib Require Export fixpoint.
+From iris.proofmode Require Import tactics.
+
+Definition bi_rtc_pre
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+    (x2 : A) (rec : A → PROP) (x1 : A) : PROP :=
+  (<affine> (x1 ≡ x2) ∨ ∃ x', R x1 x' ∗ rec x')%I.
+
+Instance bi_rtc_pre_mono
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP) `{NonExpansive2 R} (x : A) :
+  BiMonoPred (bi_rtc_pre R x).
+Proof.
+  constructor; [|solve_proper].
+  iIntros (rec1 rec2) "#H". iIntros (x1) "[Hrec | Hrec]".
+  { by iLeft. }
+  iRight.
+  iDestruct "Hrec" as (x') "[HP Hrec]".
+  iDestruct ("H" with "Hrec") as "Hrec". eauto with iFrame.
+Qed.
+
+Definition bi_rtc {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+    (x1 x2 : A) : PROP :=
+  bi_least_fixpoint (bi_rtc_pre R x2) x1.
+
+Instance: Params (@bi_rtc) 3 := {}.
+Typeclasses Opaque bi_rtc.
+
+Instance bi_rtc_ne
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+  : NonExpansive2 (bi_rtc R).
+Proof.
+  intros n x1 x2 Hx y1 y2 Hy. rewrite /bi_rtc Hx. f_equiv=> rec z.
+  solve_proper.
+Qed.
+
+Instance bi_rtc_proper
+    {PROP : sbi} {A : ofeT} (R : A → A → PROP)
+  : Proper ((≡) ==> (≡) ==> (⊣⊢)) (bi_rtc R).
+Proof. apply ne_proper_2. apply _. Qed.
+
+Section bi_rtc.
+  Context {PROP : sbi}.
+  Context {A : ofeT}.
+  Context (R : A → A → PROP) `{NonExpansive2 R}.
+
+  Lemma bi_rtc_unfold (x1 x2 : A) :
+    bi_rtc R x1 x2 ≡ bi_rtc_pre R x2 (λ x1, bi_rtc R x1 x2) x1.
+  Proof. by rewrite /bi_rtc; rewrite -least_fixpoint_unfold. Qed.
+
+  Lemma bi_rtc_strong_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ (Φ x' ∧ bi_rtc R x' x2)) -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+ Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_strong_ind (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_ind_l x2 Φ :
+    NonExpansive Φ →
+    □ (∀ x1, <affine> (x1 ≡ x2) ∨ (∃ x', R x1 x' ∗ Φ x') -∗ Φ x1) -∗
+    ∀ x1, bi_rtc R x1 x2 -∗ Φ x1.
+  Proof.
+    iIntros (?) "#IH". rewrite /bi_rtc.
+    by iApply (least_fixpoint_ind (bi_rtc_pre R x2) with "IH").
+  Qed.
+
+  Lemma bi_rtc_refl x : bi_rtc R x x.
+  Proof. rewrite bi_rtc_unfold. by iLeft. Qed.
+
+  Lemma bi_rtc_l x1 x2 x3 : R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iIntros "H1 H2".
+    iEval (rewrite bi_rtc_unfold /bi_rtc_pre). iRight.
+    iExists x2. iFrame.
+  Qed.
+
+  Lemma bi_rtc_once x1 x2 : R x1 x2 -∗ bi_rtc R x1 x2.
+  Proof. iIntros "H". iApply (bi_rtc_l with "H"). iApply bi_rtc_refl. Qed.
+
+  Lemma bi_rtc_trans x1 x2 x3 : bi_rtc R x1 x2 -∗ bi_rtc R x2 x3 -∗ bi_rtc R x1 x3.
+  Proof.
+    iRevert (x1).
+    iApply bi_rtc_ind_l.
+    { solve_proper. }
+    iIntros "!>" (x1) "[H | H] H2".
+    { by iRewrite "H". }
+    iDestruct "H" as (x') "[H IH]".
+    iApply (bi_rtc_l with "H").
+    by iApply "IH".
+  Qed.
+
+End bi_rtc.