Theorem: LeanSAT.Model.PropFun.map_neg (LeanSAT/Model/Subst.lean)

State before:
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
⊢ map f φᶜ = (map f φ)ᶜ
Tactic:
ext
State after:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f φᶜ ↔ τ✝ ⊨ (map f φ)ᶜ

State before:
case a
ν₁ : Type u_2
ν₂ : Type u_1
f : ν₁ → ν₂
φ φ₁ φ₂ : PropFun ν₁
τ✝ : PropAssignment ν₂
⊢ τ✝ ⊨ map f φᶜ ↔ τ✝ ⊨ (map f φ)ᶜ
Tactic:
simp
State after:
no goals