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).
yields error: