∀ {f : Type u → Type v} [inst : Applicative f] [toLawfulFunctor : LawfulFunctor f],
  (∀ {α β : Type u} (x : f α) (y : f β), x <* y = Function.const β <$> x <*> y) →
    (∀ {α β : Type u} (x : f α) (y : f β), x *> y = Function.const α id <$> x <*> y) →
      (∀ {α β : Type u} (g : α → β) (x : f α), pure g <*> x = g <$> x) →
        (∀ {α β : Type u} (g : α → β) (x : α), g <$> pure x = pure (g x)) →
          (∀ {α β : Type u} (g : f (α → β)) (x : α), g <*> pure x = (fun h => h x) <$> g) →
            (∀ {α β γ : Type u} (x : f α) (g : f (α → β)) (h : f (β → γ)),
                h <*> (g <*> x) = Function.comp <$> h <*> g <*> x) →
              LawfulApplicative f