∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Prop)
  (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)),
  (x = none → motive none) →
    (∀ (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n), x = some c → motive (some c)) → motive x