next l hc =>
have hsize : (Array.modify f.assignments l.1 addPosAssignment).size = n := by
  rw [Array.modify_preserves_size, f_readyForRupAdd.2.1]
refine ⟨f_readyForRupAdd.1, hsize, ?_⟩
intro i b hb
have hf := f_readyForRupAdd.2.2 i b
have i_in_bounds : i.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact i.2.2
have l_in_bounds : l.1 < f.assignments.size := by rw [f_readyForRupAdd.2.1]; exact l.2.2
simp only at hb
by_cases (i, b) = (l, true)
. next ib_eq_c =>
  simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
    List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
  apply Or.inl ∘ Or.inr
  rw [isUnit_iff, DefaultClause.toList, ← ib_eq_c] at hc
  apply DefaultClause.ext
  simp only [unit, hc]
. next ib_ne_c =>
  have hb' : hasAssignment b (f.assignments[i.1]'i_in_bounds) := by
    by_cases l.1 = i.1
    . next l_eq_i =>
      have b_eq_false : b = false := by
        by_cases b = true
        . next b_eq_true =>
          simp only [b_eq_true, Subtype.ext l_eq_i, not_true] at ib_ne_c
        . next b_eq_false =>
          simp only [Bool.not_eq_true] at b_eq_false
          exact b_eq_false
      simp only [hasAssignment, b_eq_false, l_eq_i, Array.get_modify_at_idx i_in_bounds, ite_false, hasNeg_of_addPos] at hb
      simp only [hasAssignment, b_eq_false, ite_false, hb]
    . next l_ne_i =>
      simp only [Array.get_modify_unchanged l_in_bounds i_in_bounds _ l_ne_i] at hb
      exact hb
  specialize hf hb'
  simp only [toList, Array.toList_eq, List.append_assoc, List.mem_append, List.mem_filterMap, id_eq,
    exists_eq_right, List.mem_map, Prod.exists, Bool.exists_bool] at hf
  simp only [toList, Array.toList_eq, Array.push_data, List.append_assoc, List.mem_append, List.mem_filterMap,
    List.mem_singleton, id_eq, exists_eq_right, Option.some.injEq, List.mem_map, Prod.exists, Bool.exists_bool]
  rcases hf with hf | hf
  . exact Or.inl $ Or.inl hf
  . exact Or.inr hf
case h_2
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
l✝ : PosFin n
heq✝ : c.isUnit = some (l✝, true)
⊢ { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments := f.assignments.modify l✝.val addPosAssignment }.readyForRupAdd
no goals