simp only [ne_eq, Bool.not_eq_true, exists_and_right] at h
case mk.mk.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
h :
  let assignments_i := (f.insertRupUnits units).fst.assignments[↑⟨li.val, ⋯⟩];
  let original_assignments_i := f.assignments[↑⟨li.val, ⋯⟩];
  (assignments_i = original_assignments_i ∧
      ∀ (j : Fin (f.insertRupUnits units).fst.rupUnits.size),
        (f.insertRupUnits units).fst.rupUnits[j].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
    (∃ j b i_gt_zero,
        (f.insertRupUnits units).fst.rupUnits[j] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, b) ∧
          assignments_i = addAssignment b original_assignments_i ∧
            ¬hasAssignment b original_assignments_i = true ∧
              ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                k ≠ j → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRupUnits units).fst.rupUnits[j1] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, true) ∧
          (f.insertRupUnits units).fst.rupUnits[j2] = (⟨↑⟨li.val, ⋯⟩, ⋯⟩, false) ∧
            assignments_i = both ∧
              original_assignments_i = unassigned ∧
                ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                  k ≠ j1 → k ≠ j2 → (f.insertRupUnits units).fst.rupUnits[k].fst.val ≠ ↑⟨li.val, ⋯⟩
⊢ False
case mk.mk.intro
n : Nat
f : DefaultFormula n
f_readyForRupAdd : f.readyForRupAdd
units : List (Literal (PosFin n))
i j : Fin (f.insertRupUnits units).fst.rupUnits.size
i_ne_j : i ≠ j
li : PosFin n
bi : Bool
hi : (f.insertRupUnits units).fst.rupUnits[i] = (li, bi)
lj : PosFin n
bj : Bool
hj : (f.insertRupUnits units).fst.rupUnits[j] = (lj, bj)
li_eq_lj : li = lj
bi_eq_bj : bi = bj
h :
  ((f.insertRupUnits units).fst.assignments[li.val] = f.assignments[li.val] ∧
      ∀ (j : Fin (f.insertRupUnits units).fst.rupUnits.size),
        ¬(f.insertRupUnits units).fst.rupUnits[j].fst.val = li.val) ∨
    (∃ j b,
        (∃ x, (f.insertRupUnits units).fst.rupUnits[j] = (⟨li.val, ⋯⟩, b)) ∧
          (f.insertRupUnits units).fst.assignments[li.val] = addAssignment b f.assignments[li.val] ∧
            hasAssignment b f.assignments[li.val] = false ∧
              ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                ¬k = j → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val) ∨
      ∃ j1 j2 i_gt_zero,
        (f.insertRupUnits units).fst.rupUnits[j1] = (⟨li.val, ⋯⟩, true) ∧
          (f.insertRupUnits units).fst.rupUnits[j2] = (⟨li.val, ⋯⟩, false) ∧
            (f.insertRupUnits units).fst.assignments[li.val] = both ∧
              f.assignments[li.val] = unassigned ∧
                ∀ (k : Fin (f.insertRupUnits units).fst.rupUnits.size),
                  ¬k = j1 → ¬k = j2 → ¬(f.insertRupUnits units).fst.rupUnits[k].fst.val = li.val
⊢ False