Function exists_finally 

pub fn exists_finally(
    graph: &[NQuin],
    start: u64,
    prop: u64,
    next: u64,
    holds: u64,
) -> bool

EF φ — from start, SOME path eventually reaches a state satisfying prop. Zero-heap BFS over next edges.