rw[hpq]
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ f^[↑(f p)] p = f^[↑(f q)] q
f : ℕ+ → ℕ+
hf : ∀ (n : ℕ+), f^[↑(f n)] n * f (f n) = n ^ 2
p q : ℕ+
hpq : f p = f q
h1 : f^[2] p = f^[2] q
h2 : ∀ (n : ℕ+), f^[↑n] p = f^[↑n] q
⊢ f^[↑(f q)] p = f^[↑(f q)] q