How to make a proof available for Tuple if it exists for EmptyTuple and *:?

[s5bug]

Take this method of proving that Map[T, F ∘ G] is equivalent to Map[Map[T, G], F]:

given simplifyMapMapBase[F[_], G[_]]: (Tuple.Map[EmptyTuple, [X] =>> F[G[X]]] =:= Tuple.Map[Tuple.Map[EmptyTuple, G], F]) =
  <:<.refl[EmptyTuple]

given simplifyMapMapInductive[H, T <: Tuple, F[_], G[_]](
  using simplifyMapMapTail: Tuple.Map[T, [X] =>> F[G[X]]] =:= Tuple.Map[Tuple.Map[T, G], F]
): (Tuple.Map[H *: T, [X] =>> F[G[X]]] =:= Tuple.Map[Tuple.Map[H *: T, G], F]) = {
  val expandCompose: Tuple.Map[H *: T, [X] =>> F[G[X]]] =:= (F[G[H]] *: Tuple.Map[T, [X] =>> F[G[X]]]) =
    <:<.refl[F[G[H]] *: Tuple.Map[T, [X] =>> F[G[X]]]]
  
  val expandUnsimple: Tuple.Map[Tuple.Map[H *: T, G], F] =:= (F[G[H]] *: Tuple.Map[Tuple.Map[T, G], F]) =
    <:<.refl[F[G[H]] *: Tuple.Map[Tuple.Map[T, G], F]]
  
  val prependFgh: (F[G[H]] *: Tuple.Map[T, [X] =>> F[G[X]]]) =:= (F[G[H]] *: Tuple.Map[Tuple.Map[T, G], F]) =
    simplifyMapMapTail.liftCo[[x] =>> x match { case Tuple => F[G[H]] *: x }]
  
  expandCompose.andThen(prependFgh).andThen(expandUnsimple.flip)
}

It doesn't make a proof available for X <: Tuple, that is

def proof[F[_], G[_], X <: Tuple]: Map[X, [x] =>> F[G[x]]] =:= Map[Map[X, G], F] = summon

fails.

While it is possible that one might call proof[F, G, Tuple] (or some other case that's irreducible), is there a way to prove that they're irreducible in the same way, and get a general proof out?

cc @Adam-Vandervorst