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

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

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

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