simp only [toList, Array.toList_eq, List.append_assoc,
  HSat.eval, List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe,
  List.all_eq_true, List.mem_append, List.mem_filterMap, id_eq, exists_eq_right, List.mem_map] at hp
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ((f.insertRatUnits units).fst.toList.all fun s =>
      decide (((Clause.toList s).any fun l => decide (p l.fst = l.snd)) = true)) =
    true
⊢ p ⊨ (i, b)
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
units : List (Literal (PosFin n))
h :
  let assignments := (f.insertRatUnits units).fst.assignments;
  let_fun hsize := ⋯;
  let ratUnits := (f.insertRatUnits units).fst.ratUnits;
  insertUnit_invariant f.assignments ⋯ ratUnits assignments hsize
hsize : (f.insertRatUnits units).fst.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b (f.insertRatUnits units).fst.assignments[i.val] = true
p : PosFin n → Bool
hp :
  ∀ (x : DefaultClause n),
    (some x ∈ (f.insertRatUnits units).fst.clauses.data ∨
        (∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.rupUnits.data ∧ unit (a, true) = x) ∨
          ∃ a,
            (a, false) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, false) = x ∨
              (a, true) ∈ (f.insertRatUnits units).fst.ratUnits.data ∧ unit (a, true) = x) →
      ∃ a, (a, false) ∈ Clause.toList x ∧ decide (p a = false) = true ∨ (a, true) ∈ Clause.toList x ∧ p a = true
⊢ p ⊨ (i, b)