From 6fe9381c21e6700791318920afd656a22c6a32b5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 21 May 2003 13:55:42 +0000
Subject: Nouveaux tests

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4049 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 test-suite/success/Injection.v | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v
index aecb7e1f60..fd80cec6f5 100644
--- a/test-suite/success/Injection.v
+++ b/test-suite/success/Injection.v
@@ -12,3 +12,23 @@ Injection H.
 Intros.
 Apply (n_Sn x H0).
 Qed.
+
+(* Check that no tuple needs to be built *)
+Lemma l3 : (x,y:nat)
+     (existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))=
+     (existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y)))
+  -> x=y.
+Intros x y H.
+Injection H.
+Exact [H]H.
+Qed.
+
+(* Check that a tuple is built (actually the same as the initial one) *)
+Lemma l4 : (p1,p2:{O=O}+{O=O})
+    (existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2)
+  ->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2).
+Intros.
+Injection H.
+Exact [H]H.
+Qed.
+
-- 
cgit v1.2.3