by_cases hasAssignment (decide (p i = false)) (f.assignments[i.1]'(by rw [hsize]; exact i.2.2))
case intro
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))
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
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