∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X]
  {ps : DiscreteTiling.Protoset G X ιₚ} {ppt : DiscreteTiling.PlacedTile ps → Prop} (pt : DiscreteTiling.PlacedTile ps),
  (∀ (i : ιₚ) (gx : G), ppt { index := i, groupElts := ↑gx }) → ppt pt