{L : FirstOrder.Language} →
  {M : Type u_1} →
    [inst : L.Structure M] →
      {motive : L.ElementarySubstructure M → Sort u} →
        (t : L.ElementarySubstructure M) →
          ((toSubstructure : L.Substructure M) →
              (isElementary' : toSubstructure.IsElementary) →
                motive { toSubstructure := toSubstructure, isElementary' := isElementary' }) →
            motive t