Theorem: STG4.mem_pair (Game/Levels/FamInter/L03interpair.lean)

State before:
U : Type
t A B : U
⊢ t ∈ {A, B} ↔ t = A ∨ t = B
Tactic:
rfl
State after:
no goals