simp only [heq] at c_def
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := c.clause, nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data
n : Nat
arr : Array (Option (DefaultClause n))
hsize✝¹ : (ofArray arr).assignments.size = n
modified_assignments_invariant : Array Assignment → Prop :=
  fun assignments =>
    ∃ hsize, ∀ (i : PosFin n) (b : Bool), hasAssignment b assignments[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
hb : modified_assignments_invariant (mkArray n unassigned)
acc : Array Assignment
i : PosFin n
b : Bool
cOpt : Option (DefaultClause n)
c : DefaultClause n
cOpt_in_arr : some c ∈ arr.data
hsize✝ : (ofArray_fold_fn acc (some c)).size = n
l : PosFin n
heq : c.clause = [(l, false)]
i_in_bounds : i.val < acc.size
l_in_bounds : l.val < acc.size
hsize : acc.size = n
ih : ∀ (i : PosFin n) (b : Bool), hasAssignment b acc[i.val] = true → unit (i, b) ∈ (ofArray arr).toList
i_eq_l✝ : i.val = l.val
h : hasAssignment b acc[l.val].addNegAssignment = true
b_eq_false : ¬b = true
i_eq_l : i = l
c_def : c = { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ }
⊢ some { clause := [(l, false)], nodupkey := ⋯, nodup := ⋯ } ∈ arr.data