This are useful as proofmode cannot always guess in which direction
it should use ⊣⊢.