rfl and proof of termination

Stream: new members

[Daniel Lu]

i ran into some trouble in a proof and tried to reproduce the core of my question here.
consider the following, which itself typechecks fine:

def func { a : Type } : List a -> List a -> List a
  | _, [] => []
  | xs, y :: ys => y :: func ys xs
  termination_by _ x y => x.length + y.length

my intuition was that i could prove the following:

theorem test
  (x y : a)
  (xs ys : List a)
  : func (x :: xs) (y :: ys) = y :: func ys (x :: xs)
  := rfl

however, this does not work. the fact that i am trying to prove is obviously true (replacing rfl with by simp [func] fixes the error) but i'm curious about why simply using rfl does not work here. my best guess is that this has to do with the fact that func needs a termination_by clause, but i'm not sure if that's right