DeriveFunctionEquality.scala

//> using option -Ykind-projector
trait Demo {
  type LA
  type LB
  type RA
  type RB

  def x(using
      laEqLb: LA =:= LB,
      raEqRb: RA =:= RB
  ): (LA => RA) =:= (LB => RB) = {
    // start with just proof that the function itself is equivalent to itself
    // and then substitute parts step-by-step
    val base: (LA => RA) =:= (LA => RA) = summon[(LA => RA) =:= (LA => RA)]

    // replace LA in rhs
    val step1: (LA => RA) =:= (LB => RA) =
      laEqLb.substituteCo[[A] =>> (LA => RA) =:= (A => RA)](base)

    // replace RA in rhs
    val step2: (LA => RA) =:= (LB => RB) =
      raEqRb.substituteCo[[A] =>> (LA => RA) =:= (LB => A)](step1)

    step2
  }
}