{F : Type u → Type v} →
  [inst : Applicative F] →
    {G : Type u → Type w} →
      [inst_1 : Applicative G] →
        {motive : ApplicativeTransformation F G → Sort u_1} →
          (t : ApplicativeTransformation F G) →
            ((app : (α : Type u) → F α → G α) →
                (preserves_pure' : ∀ {α : Type u} (x : α), app α (pure x) = pure x) →
                  (preserves_seq' :
                      ∀ {α β : Type u} (x : F (α → β)) (y : F α), app β (x <*> y) = app (α → β) x <*> app α y) →
                    motive { app := app, preserves_pure' := preserves_pure', preserves_seq' := preserves_seq' }) →
              motive t