Theorem: LeanSAT.Model.PropAssignment.setMany_same (LeanSAT/Model/PropAssn.lean)

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
⊢ setMany τ xs τ = τ
Tactic:
ext v
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
v : ν
⊢ setMany τ xs τ v = τ v

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
xs : Finset ν
v : ν
⊢ setMany τ xs τ v = τ v
Tactic:
simp [setMany]
State after:
no goals