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