Function fair_globally 

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

Fair EG φ — an infinite path from start on which prop holds forever AND a fair state is visited infinitely often. The fairness constraint eliminates unrealistic infinite loops that make no progress. True iff some fair state — reachable from start within the prop-states that have an infinite prop-future — lies on a cycle. Bounded + zero-heap.