exact ih2 j (Nat.le_of_succ_le j_ge_idx_add_one)
case intro.inl.intro.h.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
ih1 : assignments[↑i] = f.assignments[↑i]
ih2 : ∀ (j : Fin units.size), ↑j ≥ ↑idx → ¬units[↑j].fst.val = ↑i
j : Fin units.size
j_ge_idx_add_one : ↑j ≥ ↑idx + 1
⊢ units[j].fst.val ≠ ↑i
no goals