The module Eqdep provides the following theorem
eq_rec_eq: forall (U:Type) (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.
We use the function eq_rec to define the update function.
Section update_def.
Variables (A : Set) (A_eq_dec : forall (x y : A), ({ x = y }) + ({ x <> y })).
Variables (B : A -> Set) (a : A) (v : B a) (f : forall (x : A), B x).
Definition update (x : A) : B x :=
match A_eq_dec a x with
left h => eq_rec a B v x h
| right h' => f x
end.
End update_def.
Prove the following theorem:
Theorem update_eq:
forall (A : Set) (eq_dec : forall (x y : A), ({ x = y }) + ({ x <> y }))
(B : A -> Set) (a : A) (v : B a) (f : forall (x : A), B x),
update A eq_dec B a v f a = v.