no goals
a : Code × ℕ
⊢ (rfindOpt fun b =>
      evaln (((a, b).snd, (a, b).fst.fst), (a, b).fst.snd).fst.fst
        (((a, b).snd, (a, b).fst.fst), (a, b).fst.snd).fst.snd (((a, b).snd, (a, b).fst.fst), (a, b).fst.snd).snd) =
    eval a.fst a.snd
simp [eval_eq_rfindOpt]