proposition: Lemma reds_eval: forall a v, star red a v -> isvalue v -> eval a v.
proof: Proof. induction 1; intros. - apply isvalue_eval; auto. - apply red_eval_eval with b; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)