proposition: Lemma in_idx x l: In x l -> exists j, idx x l = Some j /\ nth j l xH = x.
proof: Proof. induction l. intros []. intro Hl. simpl idx. case eqb_spec. intros <-. exists ord0. now split. destruct Hl as [<-|Hl]. congruence. intros _. apply IHl in Hl as [j [-> Hj]]. exists (ordS j). split. reflexivity. destruct j. assumption. Qed.
imports: lsyntax ordinal lset positives kat gregex syntax