have h_inductive (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) (ih : motive idx.1 acc) :=
  confirmRupHint_preserves_motive f rupHints idx acc ih
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
motive : Nat → Array Assignment × List (Literal (PosFin n)) × Bool × Bool → Prop :=
  f.confirmRupHint_fold_entails_hsat_motive
h_base : motive 0 (f.assignments, [], false, false)
h_inductive :
  ∀ (idx : Fin rupHints.size) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool),
    motive (↑idx) acc →
      f.confirmRupHint_fold_entails_hsat_motive (↑idx + 1) (confirmRupHint f.clauses acc rupHints[idx])
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant