proposition: Lemma diverges_steps_inv: forall c s c' s', diverges s c -> star red (c, s) (c', s') -> diverges s' c'.
proof: Proof. intros. apply infseq_star_inv with (c, s); auto. intros; eapply red_determ; eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)