Theorem: HTPI.inv_inv (HTPILib/Chap8Part1.lean)

State before:
U V : Type
R : Rel U V
⊢ invRel (invRel R) = R
Tactic:
rfl
State after:
no goals