test setoid_rewrite on inv_mapsto

tests/heap_lang.ref

@@ -113,6 +113,15 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
   --------------------------------------∗
   l ↦∗{1 / 2} vs ∗ l ↦∗{1 / 2} vs
   
+1 subgoal
+  
+  Σ : gFunctors
+  heapG0 : heapG Σ
+  l : loc
+  f : val → Prop
+  Heq : ∀ v : val, f v ↔ f #true
+  ============================
+  ⊢ l ↦□ (λ _ : val, f #true)
 1 subgoal
   
   Σ : gFunctors

tests/heap_lang.v

@@ -220,13 +220,21 @@ Section tests.
 
 End tests.
 
-Section notation_tests.
+Section inv_mapsto_tests.
   Context `{!heapG Σ}.
 
   (* Make sure these parse and type-check. *)
   Lemma inv_mapsto_own_test (l : loc) : ⊢ l ↦_(λ _, True) #5. Abort.
   Lemma inv_mapsto_test (l : loc) : ⊢ l ↦□ (λ _, True). Abort.
-End notation_tests.
+
+  (* Make sure [setoid_rewrite] works. *)
+  Lemma inv_mapsto_setoid_rewrite (l : loc) (f : val → Prop) :
+    (∀ v, f v ↔ f #true) →
+    ⊢ l ↦□ (λ v, f v).
+  Proof.
+    iIntros (Heq). setoid_rewrite Heq. Show.
+  Abort.
+End inv_mapsto_tests.
 
 Section printing_tests.
   Context `{!heapG Σ}.