added some rules to translate from LTL to UNITY logic
new proofs in fixpoint calculus. incomplete
deadend with fixpoint proof :(
found the mistake in my proof, the world makes sense again (i.e. I didn't prove 'false')