File: EquivDec.v

package info (click to toggle)
coq-ext-lib 0.13.0-1
  • links: PTS, VCS
  • area: main
  • in suites: forky, sid
  • size: 808 kB
  • sloc: makefile: 44; python: 31; sh: 4; lisp: 3
file content (12 lines) | stat: -rw-r--r-- 356 bytes parent folder | download 
1
2
3
4
5
6
7
8
9
10
11
12
 
From Coq.Classes Require Import EquivDec.

Theorem EquivDec_refl_left {T : Type} {c : EqDec T (@eq T)} :
  forall (n : T), equiv_dec n n = left (refl_equal _).
Proof.
  intros. destruct (equiv_dec n n); try congruence.
  Require Eqdep_dec.
  rewrite (Eqdep_dec.UIP_dec (A := T) (@equiv_dec _ _ _ c) e (refl_equal _)).
  reflexivity.
Qed.

Export EquivDec.