∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t] {F G : Type u → Type u}
  [inst_1 : Applicative F] [inst_2 : Applicative G] [LawfulApplicative F] [LawfulApplicative G]
  (η : ApplicativeTransformation F G) {α α' β β' : Type u} (f : α → F β) (f' : α' → F β'),
  (fun {α} => η.app α) ∘ bitraverse f f' = bitraverse ((fun {α} => η.app α) ∘ f) ((fun {α} => η.app α) ∘ f')