Function preceded 

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

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