have ⟨φ₁, hφ₁⟩ := φ₁.exists_rep
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
⊢ subst (φ₁ ⊔ φ₂) f = subst φ₁ f ⊔ subst φ₂ f
ν₁ : Type u_2
ν₂ : Type u_1
φ φ₁✝ φ₂ : PropFun ν₁
f f₁ : ν₁ → PropFun ν₂
τ : PropAssignment ν₂
v : ν₁
φ₁ : PropForm ν₁
hφ₁ : ⟦φ₁⟧ = φ₁✝
⊢ subst (φ₁✝ ⊔ φ₂) f = subst φ₁✝ f ⊔ subst φ₂ f