Function refines 

pub fn refines(fine: &[u64], coarse: &[u64]) -> bool

Does fine refine coarse? I.e., is there a monotone φ with coarse = φ ∘ fine? Equivalent to fine[i] ≥ fine[j] ⟹ coarse[i] ≥ coarse[j] for all i, j. Requires equal length (two levelings of the SAME proof). A true means fine is at least as fine a partition of the proof steps as coarse — the morphism fine → coarse in the category of collapses.