intro hx
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
⊢ x ∈ range (t + 1) ∧ P x = minP t P + 1 → f (P x) = f (minP t P + 1)
case e_a.a
t : ℕ
P : ℕ → ℕ
h : Balanced t P
f : ℕ → ℕ
x : ℕ
hx : x ∈ range (t + 1) ∧ P x = minP t P + 1
⊢ f (P x) = f (minP t P + 1)