intro i
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i.val] = both
i_in_bounds : i.val < f.assignments.size
⊢ insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments ⋯
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i✝ : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i✝.val] = both
i_in_bounds : i✝.val < f.assignments.size
i : Fin n
⊢ let assignments_i := f.assignments[↑i];
  let original_assignments_i := f.assignments[↑i];
  (assignments_i = original_assignments_i ∧ ∀ (j : Fin f.ratUnits.size), f.ratUnits[j].fst.val ≠ ↑i) ∨
    (∃ j b i_gt_zero,
        f.ratUnits[j] = (⟨↑i, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin f.ratUnits.size), k ≠ j → f.ratUnits[k].fst.val ≠ ↑i) ∨
      ∃ j1 j2 i_gt_zero,
        f.ratUnits[j1] = (⟨↑i, ⋯⟩, true) ∧
          f.ratUnits[j2] = (⟨↑i, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin f.ratUnits.size), k ≠ j1 → k ≠ j2 → f.ratUnits[k].fst.val ≠ ↑i