blob: 7bb3c363bb9942bdef97fe8e63fb80d507869eb7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
(* This requires cumulativity *)
Definition Type2 := Type.
Definition Type1 := Type : Type2.
Goal (True->Type1)->Type2.
Intro H.
Apply H.
Lemma gg : (A:Type)(P:A->Type)(x:A)((y:A)(x==y)->(P y))->(P x).
Auto.
Qed.
Lemma titi : (P:Prop)P.
Intro P ; Pattern P.
Apply gg.
Qed.
|
