proposition: Lemma sos_star_f : forall r i r' i', sos_star r i i' r' -> exists n, f_star n r i = Some(r', i').
proof: Proof. induction 1. exists 0%nat; simpl; auto. case_eq (eq_skip i); intros Hi Hi'. rewrite Hi in H; inversion H. destruct IHsos_star as [n Hn]; exists (S n); simpl; rewrite Hi'. rewrite sos_step_f_sos with (1:= H); auto. Qed.
imports: ZArith List syntax Lia