Concatenation of undef and list is undef - proof Haskell

Question

How could one prove that the following is true for every list xs:

undefined ++ xs = undefined

Answer 1

There is not much to prove. There is simply a rule (which can't be explained or broken down into anything smaller) that case statements which try to match undefined against a constructor result in undefined. Once you accept this rule, we can observe

undefined ++ ys
= { by definition of ++ }
case undefined of
    [] -> ys
    x:xs -> x : (xs ++ ys)
= { case that matches undefined against a constructor }
undefined