let motive := fun (_ : Nat) (acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool) =>
  ∃ hsize : acc.1.size = n, derivedLits_invariant f f_assignments_size acc.1 hsize acc.2.1
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
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst
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
⊢ let rupCheckRes := f.performRupCheck rupHints;
  f.derivedLits_invariant f_assignments_size rupCheckRes.fst.assignments f'_assignments_size rupCheckRes.snd.fst