Theorem: LeanSAT.Model.PropForm.subst_assoc (LeanSAT/Model/Subst.lean)

State before:
ν₁ : 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₂
Tactic:
induction φ <;> simp [subst, *]
State after:
no goals