eq_rec as an identity function

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.

Solution