proposition: Lemma red_eval_eval: forall a1 a2, red a1 a2 -> forall v, eval a2 v -> eval a1 v.
proof: Proof. induction 1; intros v' E. - eauto using eval, isvalue_eval. - eauto using eval. - inversion E; subst; eauto using eval. - inversion E; subst; eauto using eval, isvalue_eval. - inversion E; subst; eauto using eval. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)