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

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