The authority is encoded once, in the canonical choice identity. That
anchor names the owner in both route fields; real announcements substitute
their own sender/receiver while preserving every other identity component.
158def protocolInformed =
159 (lambda erased payload : Type 0 .
160 (lambda unrestricted anchor : (family RegionTransferIdentity) .
161 (lambda unrestricted announcements : (family ProtocolAnnouncements payload) .
162 (lambda unrestricted role : Nat .
163 (naturalOr
164 (naturalEqual role (regionTransferSender anchor))
165 (eliminate
166 ProtocolAnnouncements
167 (lambda unrestricted current : (family ProtocolAnnouncements payload) . Nat)
168 announcements
169 (branch ProtocolAnnouncementsEnd . 0)
170 (branch
171 ProtocolAnnouncementsNext
172 identity
173 value
174 rest
175 induction
176 .
177 (naturalOr (naturalEqual role (regionTransferReceiver identity)) induction))))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.