Propagated the labelled transitions to the manually modified model and
the monadic proofs.