. next h =>
  specialize f_assignments_invariant h p pf
  by_cases hpi : p i <;> simp [hpi, HSat.eval] at f_assignments_invariant
case pos
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false

case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
case neg
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
i : PosFin n
f_assignments_invariant :
  hasAssignment (decide (p i = false)) f.assignments[i.val] = true → limplies (PosFin n) f (i, decide (p i = false))
h✝ : ¬hasAssignment (decide (p i = false)) f.assignments[i.val] = true
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false