blob: 873d2f9f7e4e0fbeb67628a9a4393e7c85d7c911 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(* Example by Jonathan Leivant, congruence and tauto up to universes *)
Variables S1 S2 : Set.
Goal @eq Type S1 S2 -> @eq Type S1 S2.
intro H.
tauto.
Qed.
Definition T1 : Type := S1.
Definition T2 : Type := S2.
Goal T1 = T1.
congruence.
Undo.
tauto.
Undo.
unfold T1.
congruence.
Undo.
tauto.
Qed.
|
