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

State before:
U V : Type
R : Rel U V
u : U
v : V
⊢ invRel R v u ↔ R u v
Tactic:
rfl
State after:
no goals