CTL is a layered definition, some low-level things should be made opaque to hide the complexity. - [ ] Opaque `ktrans` - [ ] Opaque `entailsF`