theory Scratch
  imports Main
begin

lemma 
  assumes "rl = rev l"
  shows "length l = length rl"
  using assms
proof (induction l)
  case (Cons a l)
  thm Cons.IH (* Exists *)
  oops

lemma 
  assumes "rl \<equiv> rev l"
  shows "length l = length rl"
  using assms
proof (induction l)
  case (Cons a l)
  thm Cons.IH (* Does not exist *)
  oops

end