Decidable Equality and Type Equality

Require Import Eqdep_dec_defined.
(** Same as Eqdep_dec but s/Qed/Defined/ **)

Theorem dep_destruct :
  forall (T : Type) (T' : T -> Type) x (v : T' x) (P : T' x -> Type),
    (forall x' (v' : T' x') (Heq : x' = x),
      P (match Heq in (_ = x) return (T' x) with
           | refl_equal => v'
         end)) ->
      P v.
  intros T T' x v P I; apply (I _ v (refl_equal _)).
Defined.
(** Stolen from http://www.cs.harvard.edu/~adamc/cpdt/ **)

Inductive type : Set :=
| Nat : type
| Arrow : type -> type -> type.

Definition eq_type_dec' (s t : type) : s = t \/ s <> t.
decide equality.
Defined.

Inductive equand : type -> Set :=
| Zero : equand Nat
| Succ : equand (Arrow Nat Nat).

Definition eq_equand_dec {T} (x y : equand T) : {x = y} + {x <> y}.
intro.
destruct x;
  intro y; apply (dep_destruct type equand _ y);
    intros T y' Teq; destruct y';
      discriminate ||
        rewrite <- (eq_proofs_unicity eq_type_dec' (refl_equal _) Teq).
left; reflexivity.
left; reflexivity.
Defined.