cases hφ₂
case refl
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₂✝ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
hφ₂ : ⟦φ₂⟧ = φ₂✝
⊢ subst (⟦φ₁⟧ ⊔ φ₂✝) f = subst ⟦φ₁⟧ f ⊔ subst φ₂✝ f
case refl.refl
ν₁ : Type u_2
ν₂ : Type u_1
φ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ φ₂ : PropForm ν₁
⊢ subst (⟦φ₁⟧ ⊔ ⟦φ₂⟧) f = subst ⟦φ₁⟧ f ⊔ subst ⟦φ₂⟧ f