Theorem: HTPI.rep_image_step (HTPILib/Chap6.lean)

State before:
A : Type
f : A → A
n : ℕ
B : Set A
⊢ rep_image f (n + 1) B = image f (rep_image f n B)
Tactic:
rfl
State after:
no goals