rw [Array.modify_preserves_size]
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ (acc.fst.modify l.fst.val (addAssignment l.snd)).size = n
n : Nat
f : DefaultFormula n
f_assignments_size : f.assignments.size = n
acc : Array Assignment × List (Literal (PosFin n)) × Bool × Bool
hsize : acc.fst.size = n
l : Literal (PosFin n)
ih : f.derivedLits_invariant f_assignments_size acc.fst hsize acc.snd.fst
h : ¬hasAssignment l.snd acc.fst[l.fst.val]! = true
⊢ acc.fst.size = n