exact h
case intro
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
rupHints : Array Nat
f'_assignments_size : (f.performRupCheck rupHints).fst.assignments.size = n
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  fun x acc => ∃ hsize, f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (i : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑i) acc →
      let rupHint_res := confirmRupHint f.clauses acc rupHints[i];
      ∃ hsize, f.derivedLits_invariant f_assignments_size rupHint_res.fst hsize rupHint_res.snd.fst
w✝ : (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst.size = n
h :
  f.derivedLits_invariant f_assignments_size
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).fst w✝
    (Array.foldl (fun b => confirmRupHint f.clauses b) (f.assignments, [], false, false) rupHints 0).snd.fst
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
no goals