. constructor
  . simp only [hasAssignment, hasNegAssignment, ih4, ite_false, not_false_eq_true]
  . intro k k_ge_idx_add_one k_ne_j2
    intro h1
    by_cases units[k.1].2
    . next h2 =>
      have k_ne_j1 : k ≠ j1 := by
        rw [← idx_eq_j1]
        intro k_eq_idx
        rw [k_eq_idx] at k_ge_idx_add_one
        exact Nat.lt_irrefl idx.1 $ Nat.lt_of_succ_le k_ge_idx_add_one
      have h3 := units_nodup k j1 k_ne_j1
      simp only [Fin.getElem_fin, ih1, ← h1, ← h2, ne_eq] at h3
      exact h3 rfl
    . next h2 =>
      have h3 := units_nodup k j2 k_ne_j2
      simp only [Bool.not_eq_true] at h2
      simp only [Fin.getElem_fin, ih2, ← h1, ← h2, ne_eq] at h3
      exact h3 rfl
case right.right.right
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
units : Array (Literal (PosFin n))
units_nodup : ∀ (i j : Fin units.size), i ≠ j → units[i] ≠ units[j]
idx : Fin units.size
assignments : Array Assignment
hsize : assignments.size = n
hsize' : (clearUnit assignments units[idx]).size = n
i : Fin n
j1 : Fin units.size
j1_ge_idx : ↑j1 ≥ ↑idx
j2 : Fin units.size
j2_ge_idx : ↑j2 ≥ ↑idx
i_gt_zero : ↑i > 0
ih1 : units[↑j1] = (⟨↑i, ⋯⟩, true)
ih2 : units[↑j2] = (⟨↑i, ⋯⟩, false)
ih3 : assignments[↑i] = both
ih4 : f.assignments[↑i] = unassigned
ih5 : ∀ (k : Fin units.size), ↑k ≥ ↑idx → ¬k = j1 → ¬k = j2 → ¬units[↑k].fst.val = ↑i
idx_eq_j1 : idx = j1
idx_ne_j2 : idx ≠ j2
⊢ ¬hasAssignment false f.assignments[↑i] = true ∧ ∀ (k : Fin units.size), ↑k ≥ ↑idx + 1 → k ≠ j2 → units[k].fst.val ≠ ↑i
no goals