∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} {inst : Group G} {inst_1 : MulAction G X}
  (motive : DiscreteTiling.Protoset G X ιₚ → Prop) (h : DiscreteTiling.Protoset G X ιₚ),
  (∀ (tiles : ιₚ → DiscreteTiling.Prototile G X), motive { tiles := tiles }) → motive h