Implement `outline` for one-sided program logics

[fdupress]

This might require unifying our approaches to transitivity and the variant of conseq that does transitivity for one-sided program logics.