exact Fin.elim0 j
case h
n : Nat
f : DefaultFormula n
hf : f.ratUnits = #[] ∧ f.assignments_invariant
c : DefaultClause n
p : PosFin n → Bool
pf : p ⊨ f
insertUnit_fold_success : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).2.snd = true
i✝ : PosFin n
hboth : (List.foldl insertUnit (f.ratUnits, f.assignments, false) c.negate).snd.fst[i✝.val] = both
i_in_bounds : i✝.val < f.assignments.size
i : Fin n
j✝ : Fin f.ratUnits.size
j : Fin #[].size
⊢ ¬f.ratUnits[↑j✝].fst.val = ↑i
no goals