∀ {w : ℕ} (expr : Std.Tactic.BVDecide.BVExpr w)
  (motive : Option (Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → Sort u_1)
  (h_1 : (refs : Vector Std.Sat.AIG.Fanin { w := w, expr := expr }.w) → none = some refs → motive (some refs))
  (h_2 : none = none → motive none),
  (match h : none with
    | some refs => h_1 refs h
    | none => h_2 h) =
    h_2 ⋯