I needed the lemma prefix_prefix_eq for MLS*, and the lemma prefix_prefix_grows is borrowed from the branch label_before.
The lemma prefix_prefix_eq is useful to reason on things that happened before some time, e.g. is_publishable (prefix tr time) b. It ensures that when tr grows, the prefix stays the same hence the property stays true.
I needed the lemma
prefix_prefix_eqfor MLS*, and the lemmaprefix_prefix_growsis borrowed from the branchlabel_before.The lemma
prefix_prefix_eqis useful to reason on things that happened before some time, e.g.is_publishable (prefix tr time) b. It ensures that whentrgrows, the prefix stays the same hence the property stays true.