rw [←h₂]
h₁ : ∀ (a : vset F α) (ρ : SPL.Config F), f₁ (a | ρ) = f₁' a | ρ
h₂ : ∀ (b : vset F β) (ρ : SPL.Config F), f₂ (b | ρ) = f₂' b | ρ
a : vset F α
ρ : SPL.Config F
⊢ f₂ (f₁' a | ρ) = f₂' (f₁' a) | ρ
no goals