induction φ <;> (simp [map, PropAssignment.map] at *) <;> (simp [*])
ν₁ : Type u_1
ν₂ : Type u_2
f✝ : ν₁ → ν₂
φ✝ φ₁ φ₂ φ : PropForm ν₁
f : ν₁ → ν₂
τ : PropAssignment ν₂
⊢ τ ⊨ map f φ ↔ PropAssignment.map f τ ⊨ φ
no goals