rw [PropFun.satisfies_mk]
case var
ν₁ : Type u_1
ν₂ : Type u_2
ν₃ : Type ?u.10308
f✝ f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
f : ν₁ → PropForm ν₂
τ : PropAssignment ν₂
x✝ : ν₁
⊢ τ ⊨ f x✝ ↔ τ ⊨ ⟦f x✝⟧
no goals