Proof terms for LTL Checker

[symbiont-daniel-gustafsson]

Currently the LTL checker just returns a Bool so we don't get any more information other than that the check worked or not. It would be good to have a reason for why a check failed, for example if you have always P it would be good to know at what logical time P failed if the whole formula failed.

A general idea is to move all the negation to the atoms, and for the atoms could give a reason for why the predicate failed. This is something similar to what we did in quickcheck-statemachine https://github.com/advancedtelematic/quickcheck-state-machine/blob/2515c206c5ce6795d01930027edfe69b19a66c8e/src/Test/StateMachine/Logic.hs#L103