Add equality lemmas for sig2 and sigT2

1 files changed, 11 insertions, 1 deletions

diff --git a/test-suite/success/InversionSigma.v b/test-suite/success/InversionSigma.v
index c19939eabe..51f33c7ce7 100644
--- a/test-suite/success/InversionSigma.v
+++ b/test-suite/success/InversionSigma.v
@@ -1,6 +1,6 @@
 Section inversion_sigma.
   Local Unset Implicit Arguments.
-  Context A (B : A -> Prop) (C : forall a, B a -> Prop)
+  Context A (B : A -> Prop) (C C' : forall a, B a -> Prop)
           (D : forall a b, C a b -> Prop) (E : forall a b c, D a b c -> Prop).
 
   (* Require that, after destructing sigma types and inverting
@@ -11,6 +11,8 @@ Section inversion_sigma.
     repeat match goal with
            | [ H : sig _ |- _ ] => destruct H
            | [ H : sigT _ |- _ ] => destruct H
+           | [ H : sig2 _ _ |- _ ] => destruct H
+           | [ H : sigT2 _ _ |- _ ] => destruct H
            end; simpl in *;
     inversion_sigma;
     repeat match goal with
@@ -27,4 +29,12 @@ Section inversion_sigma.
   Goal forall (x y : { a : A | { b : { b : B a | C a b } | { d : D a (proj1_sig b) (proj2_sig b) | E _ _ _ d } } })
               (p : x = y), p = p.
   Proof. test_inversion_sigma. Qed.
+
+  Goal forall (x y : { a : { a : A & B a } & C _ (projT2 a) & C' _ (projT2 a) })
+              (p : x = y), p = p.
+  Proof. test_inversion_sigma. Qed.
+
+  Goal forall (x y : { a : { a : A & B a } | C _ (projT2 a) & C' _ (projT2 a) })
+              (p : x = y), p = p.
+  Proof. test_inversion_sigma. Qed.
 End inversion_sigma.