induction φ <;> simp [subst, *]
ν₁ : Type u_3
ν₂ : Type u_2
ν₃ : Type u_1
f f₁ : ν₁ → PropForm ν₂
f₂ : ν₂ → PropForm ν₃
φ φ₁ φ₂ : PropForm ν₁
⊢ subst (subst φ f₁) f₂ = subst φ fun v => subst (f₁ v) f₂
no goals