proposition: Lemma red_progress: forall c s, c = SKIP \/ exists c', exists s', red (c, s) (c', s').
proof: Proof. induction c; intros. - auto. - right; do 2 econstructor; apply red_assign. - right. destruct (IHc1 s) as [E | (c1' & s' & R)]. + subst c1. do 2 econstructor; apply red_seq_done. + do 2 econstructor; apply red_seq_step; eauto. - right. do 2 econstructor; apply red_ifthenelse. - right. destruct (beval b s) eqn:B. + do 2 econstructor; apply red_while_loop; auto. + do 2 econstructor; apply red_while_done; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)