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

State before:
A : Type
F : Set (A → A)
n : ℕ
B : Set A
⊢ rep_image_family F (n + 1) B = {x | ∃ f ∈ F, x ∈ image f (rep_image_family F n B)}
Tactic:
rfl
State after:
no goals