From f9cc68804081ec46fc324252d74cca21f768b614 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 21 Jul 2021 18:53:00 +0200
Subject: [PATCH] Test case for equivalence on prod.

---
 tests/proper.v | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/tests/proper.v b/tests/proper.v
index becefdc8..58f68d1e 100644
--- a/tests/proper.v
+++ b/tests/proper.v
@@ -1,4 +1,4 @@
-From stdpp Require Import prelude fin_maps.
+From stdpp Require Import prelude fin_maps propset.
 
 (** Some tests for solve_proper. *)
 Section tests.
@@ -69,3 +69,7 @@ Section map_tests.
     Proper ((≡) ==> (≡@{M _})) (omap f).
   Proof. solve_proper. Qed.
 End map_tests.
+
+Lemma test_prod_equivalence (X1 X2 X3 Y : propset nat * propset nat) :
+  X3 ≡ X2 → X2 ≡ X1 → (X1,Y) ≡ (X3,Y).
+Proof. intros H1 H2. by rewrite H1, <-H2. Qed.
-- 
GitLab