How to define the restriction of a function to a smaller domain, i.e. the function projection

Question

I have defined the restriction of a function to a smaller domain in this way:

First, a valuation is a partial function that maps a variable to its interpretation in an universe 'a

type_synonym 'a Valuation = "Variable ⇀ 'a"

Second, the projection of f over U is as follows:

definition projectVal :: "'a Valuation ⇒ Variable set ⇒ 'a Valuation" where

"projectVal f U =

(

    λx. if  U ⊆ dom(f) ∧ x ∈ U then f x else undefined
)"

However, with this definition is difficult to prove a lemma like this:

lemma projectVal_Lemma:

  assumes "U ⊆ dom(f)"

  shows "dom(projectVal f U) = U" 

Even, I cannot prove the next lemma!!:

lemma domain_iff_not_undefined:

  shows "(∀f x. x ∈ dom f ⟷ f x ≠ undefined)"