Are self defined functions considered?

[DDDOH]

For example, I define a new concept

def isPalindrome (xs : List Nat) : Prop := xs = xs.reverse

and a theorem based on it

theorem test3 : isPalindrome (dup 3 [1]) := by simp [dup]; rfl

During extracting, will isPalindrome get translated to its original definition (xs = xs.reverse)?

[yangky11]

I don't think isPalindrome will be expanded to its definition