apply Exists.intro hsize'
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ (f.deleteOne id).strong_assignments_invariant
case intro
n : Nat
f : DefaultFormula n
id : Nat
hsize : f.assignments.size = n
hf : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
hsize' : (f.deleteOne id).assignments.size = n
⊢ ∀ (i : PosFin n) (b : Bool),
    hasAssignment b (f.deleteOne id).assignments[i.val] = true → unit (i, b) ∈ (f.deleteOne id).toList