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

State before:
A : Type
f : A → A → A
B : Set A
⊢ rep_un_image2 f 0 B = B
Tactic:
rfl
State after:
no goals