∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1)
  (cOpt : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) (h_1 : Unit → motive none)
  (h_2 : (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → motive (some c)),
  cOpt = none →
    (match cOpt with
      | none => h_1 ()
      | some c => h_2 c) ≍
      h_1 ()