Theorem: HTPI.Rel_prod_def (HTPILib/Chap8Part2.lean)

State before:
U V W X : Type
R : Rel U V
S : Rel W X
u : U
v : V
w : W
x : X
⊢ (R ×ᵣ S) (u, w) (v, x) ↔ R u v ∧ S w x
Tactic:
rfl
State after:
no goals