Theorem: LeanSAT.Model.PropFun.satisfies_all (LeanSAT/Model/PropFun.lean)

State before:
ν : Type u_1
a : Multiset (PropFun ν)
τ : PropAssignment ν
⊢ τ ⊨ all a ↔ ∀ i ∈ a, τ ⊨ i
Tactic:
induction a using Multiset.induction with
| empty => simp [all]
| cons => simp_all [all]
State after:
no goals

State before:
case empty
ν : Type u_1
τ : PropAssignment ν
⊢ τ ⊨ all 0 ↔ ∀ i ∈ 0, τ ⊨ i
Tactic:
simp [all]
State after:
no goals

State before:
case cons
ν : Type u_1
τ : PropAssignment ν
a✝¹ : PropFun ν
s✝ : Multiset (PropFun ν)
a✝ : τ ⊨ all s✝ ↔ ∀ i ∈ s✝, τ ⊨ i
⊢ τ ⊨ all (a✝¹ ::ₘ s✝) ↔ ∀ i ∈ a✝¹ ::ₘ s✝, τ ⊨ i
Tactic:
simp_all [all]
State after:
no goals