specialize f_assignments_invariant i (decide (p i = false))
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
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