diff options
Diffstat (limited to 'test-suite/success/univers.v')
| -rw-r--r-- | test-suite/success/univers.v | 12 |
1 files changed, 7 insertions, 5 deletions
diff --git a/test-suite/success/univers.v b/test-suite/success/univers.v index 28f9fe981..0a4b284f9 100644 --- a/test-suite/success/univers.v +++ b/test-suite/success/univers.v @@ -3,15 +3,17 @@ Definition Type2 := Type. Definition Type1 := Type : Type2. -Goal (True->Type1)->Type2. +Lemma lem1 : (True->Type1)->Type2. Intro H. Apply H. +Exact I. +Qed. -Lemma gg : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). +Lemma lem2 : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x). Auto. Qed. -Lemma titi : (P:Prop)P. +Lemma lem3 : (P:Prop)P. Intro P ; Pattern P. -Apply gg. - +Apply lem2. +Abort. |