I have been learning temporal logic with TLAPS.
I noticed that in TLAPS, if we have \A x \in SomeSet : <> <<A(x)>>_vars => <> <<B(x)>>_vars and <> <<A(x)>>_vars in the assumption base and try to prove <> <<B(x)>>_vars from it, the prover fails.
However, we can prove B(x) from \A x \in SomeSet : A(x) => B(x) and A(x).
Since I have no prior experience with temporal logic, I was wondering whether this is a limitation of temporal logic itself (if it is, then why?) or a limitation of TLAPS.
Any clarification will be appreciated.