have hl (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (hsize : acc.1.size = f.assignments.size)
  (id : Nat) (_ : id ∈ rupHints.data) : (confirmRupHint f.clauses acc id).1.size = f.assignments.size := by
  have h := confirmRupHint_preserves_assignments_size f.clauses acc.1 acc.2.1 acc.2.2.1 acc.2.2.2 id
  simp only [Prod.mk.eta] at h
  rw [h, hsize]
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size
n : Nat
f : DefaultFormula n
rupHints : Array Nat
hb : (f.assignments, [], false, false).fst.size = f.assignments.size
hl :
  ∀ (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    acc.fst.size = f.assignments.size →
      ∀ (id : Nat), id ∈ rupHints.data → (confirmRupHint f.clauses acc id).fst.size = f.assignments.size
⊢ (List.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints.data).fst.size = f.assignments.size