Predicates invariant under a transposition

Equiv.predicate_swap says that interchanging two points with equivalent predicate membership preserves membership everywhere. The predicate need not be constant or decidable, and the points need not exhaust its carrier. This proof is relocated unchanged from component face surgery so vertex-identification clients can reuse it through an ordinary import.

theorem Equiv.predicate_swap {α : Type} [DecidableEq α] (p : α → Prop) (a b : α) (hab : p a ↔ p b) (x : α) : p ((swap a b) x) ↔ p x

A transposition preserves any predicate agreeing on its two interchanged points.