fact: Fixpoint idx (x: Pred) (l: list Pred): option (ord (length l)) := match l with | [] => None | y::q => if eqb_pos x y then Some ord0 else match idx x q with Some i => Some (ordS i) | None => None end end.
imports: lsyntax ordinal lset positives kat gregex syntax