diff options
| author |  Andres Erbsen <andreser@mit.edu> | 2016-08-01 11:56:28 -0400 |
|---|---|---|
| committer | Andres Erbsen <andreser@mit.edu> | 2016-08-04 11:47:51 -0400 |
| commit | 207d320101ebcf58ee9d5febf43f31aabcab7744 (patch) | |
| tree | 39cc40d734dc82ffff355b5166672c8e51dd6b20 /src/Util/Decidable.v | |
| parent | 9485009e21f65381286d8e88903e0360c04f3cc5 (diff) | |
prove eqsig_eq using hprop in Decidable.v
Diffstat (limited to 'src/Util/Decidable.v')
| -rw-r--r-- | src/Util/Decidable.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/src/Util/Decidable.v b/src/Util/Decidable.v index 3988701a8..e19e23ca4 100644 --- a/src/Util/Decidable.v +++ b/src/Util/Decidable.v @@ -97,6 +97,10 @@ Global Instance dec_eq_nat : DecidableRel (@eq nat) | 10. exact _. Defined. Global Instance dec_eq_N : DecidableRel (@eq N) | 10 := N.eq_dec. Global Instance dec_eq_Z : DecidableRel (@eq Z) | 10 := Z.eq_dec. +Lemma eqsig_eq {T} {U} {Udec:DecidableRel (@eq U)} (f g:T->U) (x x':T) pf pf' : + (exist (fun x => f x = g x) x pf) = (exist (fun x => f x = g x) x' pf') <-> (x = x'). +Proof. apply path_sig_hprop_iff; auto using UIP_dec, Udec. Qed. + Lemma Decidable_respects_iff A B (H : A <-> B) : (Decidable A -> Decidable B) * (Decidable B -> Decidable A). Proof. solve_decidable_transparent. Defined. |