Function unique_branch_match 

pub open spec fn unique_branch_match<T, C>(tag: T, branches: Seq<(T, C)>) -> bool

{
    forall |i: nat, j: nat| {
        i < branches.len() && #[trigger] branches[i as int].0 == tag
            && j < branches.len() && #[trigger] branches[j as int].0 == tag ==> i == j
    }
}