cases hφ
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ✝ : PropFun ν₁
φ : PropForm ν₁
hφ : ⟦φ⟧ = φ✝
⊢ substL (neg φ✝) f = neg (substL φ✝ f)
case refl
ν₁ : Type u_1
ν₂ : Type u_2
f : ν₁ → PropForm ν₂
φ₁ φ₂ : PropFun ν₁
v : ν₁
φ : PropForm ν₁
⊢ substL (neg ⟦φ⟧) f = neg (substL ⟦φ⟧ f)