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

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