Substitution tactic crashes when assumptions are not complete

[SimonGuilloud]

val f = function[1]
val x = variable
val y = variable
val P = formulaVariable
val Q = predicate[1]
val thm6 = Theorem(() |- ()) {
  val s1 = have (P |- (f(x) === f(y)) ) by Sorry
  assume(Q(f(x)))
  thenHave( Q(f(y)) ) by Substitution.ApplyRules(s1)

yields

8 Cut                      ( ∧(Q(f(x))), Q(f(x)), P ) ⊢ ∨(Q(f(y)))
[info]     lib.thenHave(bot) by BasicStepTactic.Weakening
[info]    Proof tactic Weakening used in.(Substitution.scala:402) did not succeed:
[info]    Conclusion cannot be trivially derived from premise.