{n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) →
    (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
      (Unit → motive none) →
        ((l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
            (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
              (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup })) →
          ((val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
              (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
                  (nodupkey :
                    ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
                  (nodup : [l].Nodup), val = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False) →
                motive (some val)) →
            motive x