proposition: Lemma red_to_ctx_red: forall a a', red a a' -> ctx_red a a'.
proof: Proof. induction 1. - apply ctx_red_intro with (C := fun x => x). apply head_red_beta; auto. constructor. - apply ctx_red_intro with (C := fun x => x). apply head_red_cond; auto. constructor. - destruct IHred. apply ctx_red_intro with (C := fun x => App (C x) a2); auto using iscontext. - destruct IHred. apply ctx_red_intro with (C := fun x => App v (C x)); auto using iscontext. - destruct IHred. apply ctx_red_intro with (C := fun x => Cond (C x) ifso ifnot); auto using iscontext. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)