{G : Type u_1} →
  {α : Type u_2} →
    [inst : Zero G] →
      [inst_1 : VAdd G α] →
        [inst_2 : MeasurableSpace α] →
          {s : Set α} →
            {μ : MeasureTheory.Measure α} →
              {motive : MeasureTheory.IsAddFundamentalDomain G s μ → Sort u} →
                (t : MeasureTheory.IsAddFundamentalDomain G s μ) →
                  ((nullMeasurableSet : MeasureTheory.NullMeasurableSet s μ) →
                      (ae_covers : ∀ᵐ (x : α) ∂μ, ∃ g, g +ᵥ x ∈ s) →
                        (aedisjoint : Pairwise (Function.onFun (MeasureTheory.AEDisjoint μ) fun g => g +ᵥ s)) →
                          motive ⋯) →
                    motive t