simp only [← hidx, Array.data_set]
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ some (unit (i, b)) ∈ (f.clauses.set ⟨id, h✝⟩ none).data
case inl.h.isTrue.intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hsize' : (f.deleteOne id).assignments.size = n
i : PosFin n
b : Bool
i_in_bounds : i.val < f.assignments.size
c : DefaultClause n
heq : f.clauses[id]! = some c
l : Literal (PosFin n)
hl : c = { clause := [l], nodupkey := ⋯, nodup := ⋯ }
l_eq_i : l.fst.val = i.val
hb✝ : hasAssignment b (removeAssignment (!b) f.assignments[i.val]) = true
l_ne_b : l.snd = !b
hb : hasAssignment b f.assignments[i.val] = true
hf : some (unit (i, b)) ∈ f.clauses.data
h✝ : id < f.clauses.size
idx : Fin f.clauses.data.length
hidx : f.clauses.data.get idx = some (unit (i, b))
⊢ f.clauses.data.get idx ∈ f.clauses.data.set id none