Theorem: HTPI.Theorem_4_2_5_3 (HTPILib/Chap4.lean)

State before:
A B : Type
R : Set (A × B)
⊢ Ran (inv R) = Dom R
Tactic:
rfl
State after:
no goals