Substitution.ApplyRules error

[SimonGuilloud]

val A = variable
val B = variable
val app = function[2]
val f = variable
val g = variable
val x = variable
val y = variable
val thm5 = Theorem(() |- ()) {
  val s1 = have((f ∈ A, x ∈ B) |- (app(f, x) === app(f, x))) by Sorry
  val s2 = have((f ∈ A, g ∈ A) |- (f===g)) by Sorry
  val s3 = have((x ∈ B, y ∈ B) |- (x===y)) by Sorry
  have((x ∈ B, y ∈ B, f ∈ A, g ∈ A) |- (app(f, x) === app(g, y))) by Substitution.ApplyRules(s2, s3)(s1)
}

yields error:

[info]   0 Sorry ( elem(x, B), elem(f, A) ) ⊢ app(f, x) = app(f, x)
[info]   1 Sorry ( elem(g, A), elem(f, A) ) ⊢ f = g
[info]   2 Sorry ( elem(y, B), elem(x, B) ) ⊢ x = y
[info]     -1 Import 0  ( elem(x, B), elem(f, A) ) ⊢ app(f, x) = app(f, x)
[info]      0 Weakening ( elem(x, B) ∧ elem(f, A), x = y, f = g ) ⊢ ∨(app(f, x) = app(f, x))
[info]     lib.thenHave(sequentAfterEq) by BasicStepTactic.LeftSubstEq.withParametersSimple(termInputs.toList, lambda(termVars, ctx.body.substituteUnsafe2(formSubstL)))
[info]    Proof tactic LeftSubstEq used in.(Substitution.scala:323) did not succeed:
[info]    Left-hand side of the conclusion + φ(s_) is not the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).