proposition: Lemma nexts_ok_R : forall q q', Rgstar q q' -> exists n, nexts n q = Some q'.
proof: Proof. intros. elim H. exists 1. simpl. case (next x). intro s. case s. intros x0 H1. rewrite (next_unicity _ _ _ H1 H0). trivial. intros. case (final_no_future _ f _ H0). exists 0. simpl;trivial. intros. case H1;case H3;intros. exists (x1 + x0). rewrite nexts_plus;auto. rewrite H5. auto. Qed.
imports: Arith Omega Relations