let motive (_idx : Nat) (acc : DefaultFormula n × Bool) := acc.1 = f
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments.size = n
p : Literal (PosFin n)
ratHints : Array (Nat × Array Nat)
motive : Nat → DefaultFormula n × Bool → Prop := fun _idx acc => acc.fst = f
⊢ let performRatCheck_fold_res :=
    Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p ratHint else (x.fst, false)) (f, true)
      ratHints 0;
  performRatCheck_fold_res.fst = f