fact: Definition measure (v: t) : nat := if isempty v then 3%nat else (Zinf.measure (low v) + Zinf.measure (high v))%nat.
imports: Coq(ZArith Psatz Bool String List FMaps) Coq(FunctionalExtensionality) CDF(Sequences IMP)