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

State before:
U V : Type
R : Rel U V
u x : U
v y : V
⊢ remove_one R u v x y ↔ x ≠ u ∧ y ≠ v ∧ (R x y ∨ R x v ∧ R u y)
Tactic:
rfl
State after:
no goals