Imported Upstream version 8.5~beta1+dfsg

1 files changed, 17 insertions, 0 deletions

diff --git a/test-suite/bugs/opened/3209.v b/test-suite/bugs/opened/3209.v
new file mode 100644
index 00000000..3203afa1
--- /dev/null
+++ b/test-suite/bugs/opened/3209.v
@@ -0,0 +1,17 @@
+Inductive eqT {A} (x : A) : A -> Type :=
+  reflT : eqT x x.
+Definition Bi_inv (A B : Type) (f : (A -> B)) :=
+  sigT (fun (g : B -> A) =>
+          sigT (fun (h : B -> A) =>
+                  sigT (fun (α : forall b : B, eqT (f (g b)) b) =>
+                          forall a : A, eqT (h (f a)) a))).
+Definition TEquiv (A B : Type) := sigT (fun (f : A -> B) => Bi_inv _ _ f).
+
+Axiom UA : forall (A B : Type), TEquiv (TEquiv A B) (eqT A B).
+Definition idtoeqv {A B} (e : eqT A B) : TEquiv A B :=
+  sigT_rect (fun _ => TEquiv A B)
+            (fun (f : TEquiv A B -> eqT A B) H =>
+               sigT_rect (fun _ => TEquiv A B)
+                         (fun g _ => g e)
+                         H)
+            (UA A B).