theory Test imports Main

begin
  
consts lookupEq :: "'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<Rightarrow> 'b option"
primrec
  "lookupEq [] l2 a = None"
  "lookupEq (x # t1) l2 a = (if (a = x) then Some(hd l2) else lookupEq t1 (tl l2) a)"

lemma lookupEq_exists:
  "\<And>ys. \<lbrakk> length xs = length ys; a \<in> set xs \<rbrakk> \<Longrightarrow> (\<exists>y. lookupEq xs ys a = Some y)"
proof (induct xs)
  case Nil thus ?case by auto
next
  case (Cons z zs) hence "\<And>ys. \<lbrakk>length zs = length ys; a \<in> set zs\<rbrakk> \<Longrightarrow> (\<exists>y. lookupEq zs ys a = Some y)" by auto