proposition: Lemma ctx_red_to_red: forall a a', ctx_red a a' -> red a a'.
proof: Proof. assert (REC: forall a a', head_red a a' -> forall C, iscontext C -> red (C a) (C a')). { intros a a' HR; induction 1. - inversion HR; subst; constructor; auto. - apply red_app_1; auto. - apply red_app_2; auto. - apply red_cond_1; auto. } destruct 1. apply REC; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)