Prove: pure f <*> x = pure (flip ($)) <*> x <*> pure f

$ : (a -> b) -> a -> b
flip : (a -> b -> c) -> b -> a -> c
flip ($) : a -> (a -> b) -> b

(.) : (b -> c) -> (a -> b) -> a -> c
(. (flip ($))) (((a->b)->b) -> c) -> a -> c

f : x -> y
$ f : ((x -> y) -> b) -> b

(($ f). (flip ($))) x -> y

idea: Any expression built from the Applicative combinators can be transformed to a canonical form

pure (flip ($)) <*> x <*> pure f
= pure ($ f) <*> (pure (flip ($)) <*> x)
= pure (.) <*> pure ($ f) <*> pure (flip ($)) <*> x
= pure (($ f).(flip ($))) <*> x
= pure f <*> x

$ : f -> v -> f(v)
flip ($) : v -> f -> f(v)

($ f).(flip ($))
=>
(f' -> f'(f)) . (v -> f'' -> f''(v))
=>
(v -> f'(f)) where f' = f'' -> f''(v)
=> v -> f(v)
=> f