fact: Definition policy_of_invocations (ch: chain) (invs: list invocation) (default: result) : result := fold_left (fun acc inv => match inv with | Rule r => acc | Policy ch' p => if chain_beq ch ch' then p else acc end) invs default.
imports: Coq.Lists.List Fiat.Narcissus.Examples.Guard.Core