∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {F : Set X} {m : ℕ},
  Set.MapsTo T F F →
    ∀ [U.IsSymm],
      0 < m → ∀ (n : ℕ), Dynamics.coverMincard T F (U.comp U) n ≤ Dynamics.coverMincard T F U m ^ (n / m + 1)