fact: Definition large_set_check alpha i j := let beta := gnaw alpha (interval i (Nat.pred j)) in match beta with | one => Ok | zero => Too_far | _ => Remaining (pp (canon beta j)) end.
imports: hydras(E0 Canon Paths MoreLists Large_Sets)