intro i
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
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
i : Fin n
⊢ let_fun i_lt_assignments_size := ⋯;
  let_fun i_lt_f_assignments_size := ⋯;
  let assignments_i := (f.assignments, [], false, false).fst[↑i];
  let fassignments_i := f.assignments[↑i];
  (assignments_i = fassignments_i ∧
      ∀ (l : Literal (PosFin n)), l ∈ (f.assignments, [], false, false).snd.fst → l.fst.val ≠ ↑i) ∨
    (∃ j,
        ((f.assignments, [], false, false).snd.fst.get j).fst.val = ↑i ∧
          assignments_i = addAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i ∧
            ¬hasAssignment ((f.assignments, [], false, false).snd.fst.get j).snd fassignments_i = true ∧
              ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                k ≠ j → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i) ∨
      ∃ j1 j2,
        ((f.assignments, [], false, false).snd.fst.get j1).fst.val = ↑i ∧
          ((f.assignments, [], false, false).snd.fst.get j2).fst.val = ↑i ∧
            ((f.assignments, [], false, false).snd.fst.get j1).snd = true ∧
              ((f.assignments, [], false, false).snd.fst.get j2).snd = false ∧
                assignments_i = both ∧
                  fassignments_i = unassigned ∧
                    ∀ (k : Fin (f.assignments, [], false, false).snd.fst.length),
                      k ≠ j1 → k ≠ j2 → ((f.assignments, [], false, false).snd.fst.get k).fst.val ≠ ↑i