∀ {α : Type u_1} [inst : DecidableEq α] {𝒜 : Finset (Finset α)} (u v : Finset α),
  (∀ x ∈ u, ∃ y ∈ v, UV.IsCompressed (u.erase x) (v.erase y) 𝒜) →
    (UV.compression u v 𝒜).shadow ⊆ UV.compression u v 𝒜.shadow