Problem.agda

data _==_ {a : Set} (x : a) : a -> Set where
  Refl : x == x

data List (a : Set) : Set where
  Nil : List a
  Cons : a -> List a -> List a

--                                                                    ~~~~~~~~~~~~~~~~~~~~~~~~ Highlighted as yellow
lemma : {a : Set} (x y : a) (xs ys : List a) -> x == y -> xs == ys -> (Cons x xs == Cons y ys)
lemma = {!!}