simp [*]
case h
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ : PropForm ν₁
inst✝² : DecidableEq ν₁
inst✝¹ : DecidableEq ν₂
inst✝ : Fintype ν₁
f : ν₁ → ν₂
hf : Function.Injective f
φ : PropForm ν₁
v1 : ν₁
left✝ : v1 ∈ vars φ
h : f v1 ∈ PropFun.semVars ⟦map f φ⟧
τ : PropAssignment ν₂
hpos : PropAssignment.map f τ ⊨ φ
hneg : ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
⊢ PropAssignment.map f τ ⊨ φ ∧ ¬(PropAssignment.set (PropAssignment.map f τ) v1 !τ (f v1)) ⊨ φ
no goals