provide a lemma to update only the authoritative part, ignoring the fragments entirely
Surprisingly, I could not find a transitivity lemma for updates either, so I added one.
Surprisingly, I could not find a transitivity lemma for updates either, so I added one.