How to prove `view` distributiveness over a lens composition

Learn
5

I believe it should be possible to prove something like

g . f Const = f (g . Const)
 where
  f :: Lens' A B
  g :: forall x. Const B x -> Const B x