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

State before:
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
⊢ set (set τ x v) x v' = set τ x v'
Tactic:
ext x'
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ set (set τ x v) x v' x' = set τ x v' x'

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ set (set τ x v) x v' x' = set τ x v' x'
Tactic:
dsimp [set]
State after:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ (if x' = x then v' else if x' = x then v else τ x') = if x' = x then v' else τ x'

State before:
case h
ν : Type u_1
inst✝ : DecidableEq ν
τ : PropAssignment ν
x : ν
v v' : Bool
x' : ν
⊢ (if x' = x then v' else if x' = x then v else τ x') = if x' = x then v' else τ x'
Tactic:
split <;> simp_all
State after:
no goals