intro ⟨hsize, h⟩
n : Nat
f : DefaultFormula n
⊢ f.strong_assignments_invariant → f.assignments_invariant
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.assignments_invariant