take TrivialLTLModel ; :: thesis: TrivialLTLModel is with_basic
thus TrivialLTLModel is with_basic ; :: thesis: verum