pub open spec fn branch_exists<T, C>(tag: T, branches: Seq<(T, C)>) -> bool
{ exists |i: nat| i < branches.len() && #[trigger] branches[i as int].0 == tag }