(acc : List Lean.Expr) →
  (motive : Option (Fin acc.length) → Sort u_1) →
    (n : Option (Fin acc.length)) →
      ((n : Fin acc.length) → motive (some n)) → ((x : Option (Fin acc.length)) → motive x) → motive n