Theorem: HTPI.rep_common_image_step (HTPILib/Chap8Part2.lean)

State before:
U V : Type
R S : Rel U V
X0 : Set U
m : ℕ
a : U
⊢ a ∈ rep_common_image R S X0 (m + 1) ↔ ∃ x ∈ rep_common_image R S X0 m, ∃ y, R x y ∧ S a y
Tactic:
rfl
State after:
no goals