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

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