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

State before:
A B : Type
R : Set (A × B)
a : A
b : B
⊢ RelFromExt R a b ↔ (a, b) ∈ R
Tactic:
rfl
State after:
no goals