intro p pf
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
⊢ limplies (PosFin n) f f.assignments
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments