First return after removing two permutation points

Removing the two Option points keeps the first retained successor. Permutation injectivity rules out revisiting a deleted point before reaching a retained point, so at most three successor steps are needed. The five possible directed paths are explicit, with no finite carrier or equality-decision assumption. This is an original elementary reconstruction for bounded rotation-certificate restriction.

theorem Equiv.Perm.removeNone_removeNone_paths {α : Type u_1} (f : Perm (Option (Option α))) (a : α) : have b := (removeNone f).removeNone a; f (some (some a)) = some (some b) ∨ f (some (some a)) = none ∧ f none = some (some b) ∨ f (some (some a)) = some none ∧ f (some none) = some (some b) ∨ f (some (some a)) = none ∧ f none = some none ∧ f (some none) = some (some b) ∨ f (some (some a)) = some none ∧ f (some none) = none ∧ f none = some (some b)

The five possible first-return paths through two removed points. In each case the retained endpoint is exactly the twice-removeNone successor; the two three-step cases preserve the order of visits to the removed points.