rw [satisfies_mk, satisfies_mk]
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ ⟦PropForm.map f ϕ⟧ ↔ PropAssignment.map f τ ⊨ ⟦ϕ⟧
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → ν₂
τ : PropAssignment ν₂
ϕ : PropForm ν₁
⊢ τ ⊨ PropForm.map f ϕ ↔ PropAssignment.map f τ ⊨ ϕ