Function terminated 

pub open spec fn terminated<FmtA, FmtB, A, B, const CHECK: bool>(
    a: FmtA,
    b: FmtB,
    b_val: B,
) -> Mapped<Refined<Pair<FmtA, FmtB>, PredFnSpec<(A, B)>>, BiMapper<(A, B), A>>

{
    Mapped {
        inner: Refined(
            Pair(a, b),
            |pair: (A, B)| if CHECK { pair.1 == b_val } else { true },
        ),
        mapper: BiMap(|pair: (A, B)| pair.0, |a| (a, b_val)),
    }
}