{w : ℕ} →
  (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) →
    (motive : Option (aig.RefVec w) → Sort u_1) →
      (x : Option (aig.RefVec w)) → ((vec : aig.RefVec w) → motive (some vec)) → (Unit → motive none) → motive x