Theorem: ClassicalPropositionalLogic.satisfies_insert_iff (GlimpseOfLean/Solutions/Topics/ClassicalPropositionalLogic.lean)

State before:
v : Variable → Prop
A B : Formula
Γ : Set Formula
⊢ Satisfies v (insert A Γ) ↔ IsTrue v A ∧ Satisfies v Γ
Tactic:
simp [Satisfies]
State after:
no goals