have h0 : insertUnit_invariant f.assignments hf.2 f.ratUnits f.assignments hsize := by
  intro i
  apply Or.inl
  simp only [Fin.getElem_fin, ne_eq, true_and, Bool.not_eq_true, exists_and_right]
  intro j
  simp only [hf.1, Array.size_toArray, List.length_nil] at j
  exact Fin.elim0 j
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
units : List (Literal (PosFin n))
hsize : f.assignments.size = n
h0 : insertUnit_invariant f.assignments ⋯ f.ratUnits f.assignments hsize
⊢ insertUnit_invariant f.assignments ⋯ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst
    (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).2.fst ⋯