∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] [inst_1 : DecidableRel Disjoint] [inst_2 : DecidableLE α]
  {s : Finset α} {u v a : α} [inst_3 : DecidableEq α], a ∈ UV.compression u v s → v ≤ a → Disjoint u a → (a ⊔ u) \ v ∈ s