simp [*]
case biImpl
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
φ₁✝ φ₂✝ : PropForm ν₁
φ₁_ih✝ : τ ⊨ map f φ₁✝ ↔ τ ∘ f ⊨ φ₁✝
φ₂_ih✝ : τ ⊨ map f φ₂✝ ↔ τ ∘ f ⊨ φ₂✝
⊢ (τ ⊨ map f φ₁✝ ↔ τ ⊨ map f φ₂✝) ↔ (τ ∘ f ⊨ φ₁✝ ↔ τ ∘ f ⊨ φ₂✝)
no goals