fact: Definition isempty (N: t) : bool := match N with | {| low := Fin l; high := Fin h |} => h <? (-l) | _ => false end.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)