{H : Type u_1} →
  {H' : Type u_3} →
    [inst : TopologicalSpace H] →
      [inst_1 : TopologicalSpace H'] →
        {G : StructureGroupoid H} →
          {G' : StructureGroupoid H'} →
            {P : (H → H') → Set H → H → Prop} →
              {motive : G.LocalInvariantProp G' P → Sort u} →
                (t : G.LocalInvariantProp G' P) →
                  ((is_local :
                        ∀ {s : Set H} {x : H} {u : Set H} {f : H → H'}, IsOpen u → x ∈ u → (P f s x ↔ P f (s ∩ u) x)) →
                      (right_invariance' :
                          ∀ {s : Set H} {x : H} {f : H → H'} {e : OpenPartialHomeomorph H H},
                            e ∈ G → x ∈ e.source → P f s x → P (f ∘ ↑e.symm) (↑e.symm ⁻¹' s) (↑e x)) →
                        (congr_of_forall :
                            ∀ {s : Set H} {x : H} {f g : H → H'},
                              (∀ y ∈ s, f y = g y) → f x = g x → P f s x → P g s x) →
                          (left_invariance' :
                              ∀ {s : Set H} {x : H} {f : H → H'} {e' : OpenPartialHomeomorph H' H'},
                                e' ∈ G' → s ⊆ f ⁻¹' e'.source → f x ∈ e'.source → P f s x → P (↑e' ∘ f) s x) →
                            motive ⋯) →
                    motive t