diff options
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/success/Injection.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/test-suite/success/Injection.v b/test-suite/success/Injection.v index aecb7e1f6..fd80cec6f 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. + |