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

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

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