diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 10:56:15 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-10-22 13:44:57 +0200 |
| commit | 4da13b45ea2da8525c7f2dc38833cf24f6f02e74 (patch) | |
| tree | 24aff9259b1032010123a7e5c31b7fa84ac45ec4 /theories/Logic | |
| parent | d856e6ea6366e148b9b215fc1ef9631c1da07320 (diff) | |
EqdepFacts: generalize statements which were wrongly restricted to Prop.
Diffstat (limited to 'theories/Logic')
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index afd0ecf04..939fbe408 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -142,7 +142,7 @@ Qed. Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing). (* Compat *) Lemma eq_sig_eq_dep : - forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), exist P p x = exist P q y -> eq_dep p x q y. Proof. intros. @@ -151,14 +151,14 @@ Proof. Qed. Lemma eq_dep_eq_sig : - forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), eq_dep p x q y -> exist P p x = exist P q y. Proof. destruct 1; reflexivity. Qed. Lemma eq_sig_iff_eq_dep : - forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q), + forall (U:Type) (P:U -> Prop) (p q:U) (x:P p) (y:P q), exist P p x = exist P q y <-> eq_dep p x q y. Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. |