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