Theorem: HTPI.Exercises.rep_image2_step (Chap6Ex.lean)

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