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

State before:
U V : Type
a x : U
b y : V
⊢ one_match a b x y ↔ x = a ∧ y = b
Tactic:
rfl
State after:
no goals