∀ {n : ℕ} (f : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n)
  (c1 c2 : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n),
  (some c2 ∈
          (match c1.isUnit with
              | none =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }
              | some (l, true) =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments :=
                    f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
              | some (l, false) =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments :=
                    f.assignments.modify (↑l)
                      Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }).clauses.toList ∨
        c2 ∈
          List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit
            (match c1.isUnit with
                | none =>
                  { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments := f.assignments }
                | some (l, true) =>
                  { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments :=
                      f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
                | some (l, false) =>
                  { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                    assignments :=
                      f.assignments.modify (↑l)
                        Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }).rupUnits.toList) ∨
      c2 ∈
        List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit
          (match c1.isUnit with
              | none =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments := f.assignments }
              | some (l, true) =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments :=
                    f.assignments.modify (↑l) Std.Tactic.BVDecide.LRAT.Internal.Assignment.addPosAssignment }
              | some (l, false) =>
                { clauses := f.clauses.push (some c1), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
                  assignments :=
                    f.assignments.modify (↑l)
                      Std.Tactic.BVDecide.LRAT.Internal.Assignment.addNegAssignment }).ratUnits.toList ↔
    c2 = c1 ∨
      (some c2 ∈ f.clauses.toList ∨
          c2 ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit f.rupUnits.toList) ∨
        c2 ∈ List.map Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.unit f.ratUnits.toList