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

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