∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ β₀ β₁ : Type u}
  (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀),
  Functor.Comp.mk (Bitraversable.tsnd f' <$> Bitraversable.tfst f x) =
    bitraverse (Functor.Comp.mk ∘ Functor.map pure ∘ f) (Functor.Comp.mk ∘ pure ∘ f') x