. apply And.intro h1 ∘ And.intro h2
  intro k _ k_ne_j1 k_ne_j2
  have k_in_bounds : k < derivedLits.length := by
    have k_property := k.2
    simp only [derivedLits_arr_def, Array.size_mk] at k_property
    exact k_property
  have k_ne_j1 : ⟨k.1, k_in_bounds⟩ ≠ j1 := by
    apply Fin.ne_of_val_ne
    simp only
    exact Fin.val_ne_of_ne k_ne_j1
  have k_ne_j2 : ⟨k.1, k_in_bounds⟩ ≠ j2 := by
    apply Fin.ne_of_val_ne
    simp only
    exact Fin.val_ne_of_ne k_ne_j2
  simp only [Fin.getElem_fin, Array.getElem_eq_data_get, ne_eq, derivedLits_arr_def]
  exact h3 ⟨k.1, k_in_bounds⟩ k_ne_j1 k_ne_j2
case inr.inr.intro.intro.intro.intro.intro.intro.intro.intro.right.right
rupHints : Array Nat
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
f' : DefaultFormula n
_f'_def : f' = (f.performRupCheck rupHints).fst
f'_assignments_size : f'.assignments.size = n
derivedLits : List (Literal (PosFin n))
derivedLits_arr : Array (Literal (PosFin n))
derivedLits_arr_def : derivedLits_arr = { data := derivedLits }
_derivedLits_arr_nodup : ∀ (i j : Fin derivedLits_arr.size), i ≠ j → derivedLits_arr[i] ≠ derivedLits_arr[j]
i : Fin n
j1 j2 : Fin derivedLits.length
j1_eq_i : (derivedLits.get j1).fst.val = ↑i
j2_eq_i : (derivedLits.get j2).fst.val = ↑i
j1_eq_true : (derivedLits.get j1).snd = true
j2_eq_false : (derivedLits.get j2).snd = false
h1 : f'.assignments[↑i] = both
h2 : f.assignments[↑i] = unassigned
h3 : ∀ (k : Fin derivedLits.length), k ≠ j1 → k ≠ j2 → (derivedLits.get k).fst.val ≠ ↑i
j1_lt_derivedLits_arr_size : ↑j1 < derivedLits_arr.size
j2_lt_derivedLits_arr_size : ↑j2 < derivedLits_arr.size
i_gt_zero : ↑i > 0
⊢ f'.assignments[↑i] = both ∧
    f.assignments[↑i] = unassigned ∧
      ∀ (k : Fin derivedLits_arr.size),
        ↑k ≥ 0 →
          k ≠ ⟨↑j1, j1_lt_derivedLits_arr_size⟩ →
            k ≠ ⟨↑j2, j2_lt_derivedLits_arr_size⟩ → derivedLits_arr[k].fst.val ≠ ↑i
no goals