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

State before:
U V W : Type
S : Rel V W
R : Rel U V
u : U
w : W
⊢ compRel S R u w ↔ ∃ x, R u x ∧ S x w
Tactic:
rfl
State after:
no goals