let motive := confirmRupHint_fold_entails_hsat_motive f
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
rupHints : Array Nat
⊢ { 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
⊢ { clauses := f.clauses, rupUnits := f.rupUnits, ratUnits := f.ratUnits,
      assignments :=
        (Array.foldl (confirmRupHint f.clauses) (f.assignments, [], false, false) rupHints
            0).fst }.assignments_invariant