diff options
Diffstat (limited to 'theories/Logic/EqdepFacts.v')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 15 |
1 files changed, 9 insertions, 6 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 0e9f39f6b..2c971ec24 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -52,6 +52,8 @@ Table of contents: Import EqNotations. +Set Universe Polymorphism. + Section Dependent_Equality. Variable U : Type. @@ -117,7 +119,7 @@ Lemma eq_sigT_eq_dep : existT P p x = existT P q y -> eq_dep p x q y. Proof. intros. - dependent rewrite H. + dependent rewrite H. apply eq_dep_intro. Qed. @@ -162,11 +164,12 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent to a dependent pair of equalities *) +(** Dependent equality is equivalent tco a dependent pair of equalities *) Set Implicit Arguments. -Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}. +Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> + {H:x1=x2 | rew H in H1 = H2}. Proof. intros; split; intro H. - change x2 with (projT1 (existT P x2 H2)). @@ -191,7 +194,7 @@ Lemma eq_sigT_snd : forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2. Proof. intros. - unfold eq_sigT_fst. + unfold eq_sigT_fst. change x2 with (projT1 (existT P x2 H2)). change H2 with (projT2 (existT P x2 H2)) at 3. destruct H. @@ -271,8 +274,8 @@ Section Equivalences. Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq. Proof. intros eq_rect_eq; red; intros. - apply (eq_rect_eq__eq_dep1_eq eq_rect_eq); apply eq_dep_dep1; trivial. - Qed. + apply (eq_rect_eq__eq_dep1_eq eq_rect_eq). apply eq_dep_dep1; trivial. + Qed. (** Uniqueness of Identity Proofs (UIP) is a consequence of *) (** Injectivity of Dependent Equality *) |