mathlib

81d6c90b - two morphisms of covering agreeing on a vertex agree on any reachable (in the symmetrified) vertex