proposition: Lemma eval_reds: forall a v, eval a v -> star red a v.
proof: Proof. induction 1. - apply star_refl. - apply star_trans with (App (Abs x a) a2). revert IHeval1. generalize a1, (Abs x a). induction 1; eauto using star, red_app_1. apply star_trans with (App (Abs x a) v2). revert IHeval2. generalize a2, v2. induction 1; eauto using star, red_app_2, isvalue. eapply star_step. apply red_beta. eapply eval_isvalue; eauto. apply IHeval3. - apply star_refl. - apply star_trans with (Cond (Const b) ifso ifnot). revert IHeval1. generalize a, (Const b). induction 1; eauto using star, red_cond_1. eapply star_step. apply red_cond. apply IHeval2. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)