proposition: Lemma nexts_ok : forall n q q', nexts n q = Some q' -> Rgstar q q'.
proof: Proof. induction n; simpl; auto. injection 1; destruct 1;constructor 2. intros q q'; case (next q). destruct s. intro. constructor 3 with x;auto. apply IHn;auto. discriminate 2. Qed.
imports: Arith Omega Relations