{L : FirstOrder.Language} →
  {T : L.Theory} →
    {α : Type w} →
      {motive : T.CompleteType α → Sort u_1} →
        (t : T.CompleteType α) →
          ((toTheory : (L.withConstants α).Theory) →
              (subset' : (L.lhomWithConstants α).onTheory T ⊆ toTheory) →
                (isMaximal' : toTheory.IsMaximal) →
                  motive { toTheory := toTheory, subset' := subset', isMaximal' := isMaximal' }) →
            motive t