proposition: Theorem update_eq: forall (A : Type) (eq_dec : forall (x y : A), { x = y } + { x <> y }) (B : A -> Type) (a : A) (v : B a) (f : forall (x : A), B x), update A eq_dec B a v f a = v.
proof: Proof. intros A eq_dec B a v f. unfold update;case (eq_dec a a). - intros e; rewrite <- eq_rect_eq;auto. - intros Hneq; elim Hneq; trivial. Qed.
imports: Eqdep