intro h x
case mpr
f g : Vars →₀ ℕ
⊢ f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ → ∀ (x : Vars), f x = g x
case mpr
f g : Vars →₀ ℕ
h : f α = g α ∧ f β_v = g β_v ∧ f β_w = g β_w ∧ f β_y = g β_y ∧ f γ = g γ
x : Vars
⊢ f x = g x