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]
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
i : PosFin n
b : Bool
hb :
  hasAssignment b
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.assignments[i.val] =
    true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ unit (i, b) ∈
    { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
        assignments := f.assignments }.toList
case h_1
n : Nat
f : DefaultFormula n
c : DefaultClause n
f_readyForRupAdd : f.readyForRupAdd
x✝ : Option (Literal (PosFin n))
heq✝ : c.isUnit = none
i : PosFin n
b : Bool
hb :
  hasAssignment b
      { clauses := f.clauses.push (some c), rupUnits := f.rupUnits, ratUnits := f.ratUnits,
            assignments := f.assignments }.assignments[i.val] =
    true
hf :
  some (unit (i, b)) ∈ f.clauses.data ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)
⊢ (some (unit (i, b)) ∈ f.clauses.data ∨ unit (i, b) = c) ∨
    (∃ a,
        (a, false) ∈ f.rupUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.rupUnits.data ∧ unit (a, true) = unit (i, b)) ∨
      ∃ a,
        (a, false) ∈ f.ratUnits.data ∧ unit (a, false) = unit (i, b) ∨
          (a, true) ∈ f.ratUnits.data ∧ unit (a, true) = unit (i, b)