simp_rw [h]
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
case mp
f g : Vars →₀ ℕ
h : ∀ (x : Vars), f x = g x
⊢ True ∧ True ∧ True ∧ True ∧ True