More on injection over a projectable "existT". - Fixing syntax "injection ... as ..." which was not working. - Now applying the simplification on any "existT" generated by "injection" (possible source of incompatibilities).

1 files changed, 32 insertions, 0 deletions

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index 9d5047fdc..6a4882443 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -84,6 +84,38 @@ injection H.
 intro H0. exact H0.
 Abort.
 
+(* Test injection using K, knowing that an equality is decidable *)
+(* Basic case, using sigT, with "as" clause *)
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  existT P n H1 = existT P n H2 -> H1 = H2.
+intros.
+injection H as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT *)
+
+Inductive my_sig (A : Type) (P : A -> Type) : Type :=
+    my_exist : forall x : A, P x -> my_sig A P.
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  my_exist _ _ n H1 = my_exist _ _ n H2 -> H1 = H2.
+intros.
+injection H as H.
+exact H.
+Abort.
+
+(* Test injection using K, knowing that an equality is decidable *)
+(* Dependent case not directly exposing sigT deeply nested *)
+
+Goal forall n:nat, forall P:nat -> Type, forall H1 H2:P n,
+  (my_exist _ _ n H1,0) = (my_exist _ _ n H2,0) -> H1 = H2.
+intros * [= H].
+exact H.
+Abort.
+
 (* Injection does not projects at positions in Prop... allow it?
 
 Inductive t (A:Prop) : Set := c : A -> t A.