fact: Fixpoint ofold X Y (f: X -> Y -> option Y) (l: list X) (y: Y): option Y := match l with | [] => Some y | x::q => obind (f x) (ofold f q y) end.
imports: lset kat positives sums glang boolean comparisons powerfix ugregex