apply Exists.intro f_assignments_size
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
⊢ motive 0 (f.assignments, [], false, false)
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
⊢ f.derivedLits_invariant f_assignments_size (f.assignments, [], false, false).fst f_assignments_size
    (f.assignments, [], false, false).snd.fst