TLAPS fails to prove instances of temporal theorems

[muenchnerkindl]

Neither of the following lemmas is proved using either OBVIOUS or PTL. The description of the coalescing algorithm for first-order temporal formulas sounds like the CONSTANT version should be provable by first-order backends.

THEOREM ASSUME CONSTANT A, TEMPORAL F(_),
ASSUME CONSTANT B PROVE □F(B)
PROVE □F(A)

THEOREM ASSUME VARIABLE A, TEMPORAL F(_),
ASSUME VARIABLE B PROVE □F(B)
PROVE □F(A)
BY PTL