∀ {F : Type u → Type v} {inst : Applicative F} {G : Type u → Type w} {inst_1 : Applicative 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}
  {app_1 : (α : Type u) → F α → G α} {preserves_pure'_1 : ∀ {α : Type u} (x : α), app_1 α (pure x) = pure x}
  {preserves_seq'_1 : ∀ {α β : Type u} (x : F (α → β)) (y : F α), app_1 β (x <*> y) = app_1 (α → β) x <*> app_1 α y},
  { app := app, preserves_pure' := preserves_pure', preserves_seq' := preserves_seq' } =
      { app := app_1, preserves_pure' := preserves_pure'_1, preserves_seq' := preserves_seq'_1 } →
    app = app_1