blob: 39b103747c554ff2d87313eabf6ef900a6b5f276 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
|
Set Universe Polymorphism.
Cumulative Inductive EQ {A} (x : A) : A -> Type
:= EQ_refl : EQ x x.
Register EQ as core.eq.type.
Lemma renamed_EQ_rect {A} (x:A) (P : A -> Type)
(c : P x) (y : A) (e : EQ x y) : P y.
Proof. destruct e. assumption. Qed.
Register renamed_EQ_rect as core.eq.rect.
Register renamed_EQ_rect as core.eq.ind.
Lemma renamed_EQ_rect_r {A} (x:A) (P : A -> Type)
(c : P x) (y : A) (e : EQ y x) : P y.
Proof. destruct e. assumption. Qed.
Register renamed_EQ_rect_r as core.eq.rect_r.
Register renamed_EQ_rect_r as core.eq.ind_r.
Lemma EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
Proof. rewrite e. reflexivity. Qed.
Lemma EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
Proof. rewrite <- e. reflexivity. Qed.
Require Import ssreflect.
Lemma ssr_EQ_sym1 {A} {x y : A} (e : EQ x y) : EQ y x.
Proof. rewrite e. reflexivity. Qed.
Lemma ssr_EQ_sym2 {A} {x y : A} (e : EQ x y) : EQ y x.
Proof. rewrite -e. reflexivity. Qed.
|
