simp only [toList, insertRatUnits, Prod.mk.eta, 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]
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
⊢ c ∈ (f.insertRatUnits units).fst.toList → c ∈ List.map Clause.unit units ∨ c ∈ f.toList
n : Nat
f : DefaultFormula n
units : List (Literal (PosFin n))
c : DefaultClause n
⊢ (some c ∈ f.clauses.data ∨
      (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
        ∃ a,
          (a, false) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧ unit (a, false) = c ∨
            (a, true) ∈ (List.foldl insertUnit (f.ratUnits, f.assignments, false) units).fst.data ∧
              unit (a, true) = c) →
    (∃ a, (a, false) ∈ units ∧ Clause.unit (a, false) = c ∨ (a, true) ∈ units ∧ Clause.unit (a, true) = c) ∨
      some c ∈ f.clauses.data ∨
        (∃ a, (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = c) ∨
          ∃ a, (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = c ∨ (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = c