{G : Type u_1} →
  {X : Type u_2} →
    [inst : AddGroup G] →
      [inst_1 : AddAction G X] →
        {motive : AddAction.IsQuasiPreprimitive G X → Sort u} →
          (t : AddAction.IsQuasiPreprimitive G X) →
            ([toIsPretransitive : AddAction.IsPretransitive G X] →
                (isPretransitive_of_normal :
                    ∀ {N : AddSubgroup G} [N.Normal],
                      AddAction.fixedPoints (↥N) X ≠ Set.univ → AddAction.IsPretransitive (↥N) X) →
                  motive ⋯) →
              motive t