Coq casts for function domains and codomains and results

With dependent types it may happen, that a theorem of the form a = b does not type-check, because you can only prove that the types of a and b are equal and the type checker does not see this equality. The workaround is to rewrite the type of a into the type of b (or vice versa), using the proven equality. On the term level this rewriting is done with a dependent pattern match on the equality proof.
Because these pattern matches are a bit verbose, I define here the casts that I need.

Definition fun_dom_cast{X Y Z : Type}(eq : X = Y)(f : X → Z) : Y → Z :=
  match eq in _ = Y' return Y' → Z with
    | eq_refl ⇒ f
  end.

Lemma dom_map_cast :
  ∀(X Y Z : Type)(T : Type → Type)
        (TM : ∀(A B : Type), (A → B) → (T A → T B))
        (eq_lift : ∀(A B : Type), A = B → T A = T B)
        (eq : X = Y)(f : X → Z),
    (∀(A : Type), eq_lift A A eq_refl = eq_refl) →
      TM Y Z (fun_dom_cast eq f) =
      fun_dom_cast (eq_lift X Y eq) (TM X Z f).

Definition fun_codom_cast{X Y Z : Type}(eq : Y = Z)(f : X → Y) : X → Z :=
  match eq in _ = Z' return X → Z' with
    | eq_refl ⇒ f
  end.

Lemma codom_map_cast :
  ∀(X Y Z : Type)(T : Type → Type)
        (TM : ∀(A B : Type), (A → B) → (T A → T B))
        (eq_lift : ∀(A B : Type), A = B → T A = T B)
        (eq : Y = Z)(f : X → Y),
    (∀(A : Type), eq_lift A A eq_refl = eq_refl) →
      TM X Z (fun_codom_cast eq f) =
      fun_codom_cast (eq_lift Y Z eq) (TM X Y f).