rcases f_assignments_invariant with ⟨hsize, f_assignments_invariant⟩
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments
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)
⊢ p ⊨ f.assignments