proposition: Theorem red_denot: forall E t a1 a2, red E t a1 a2 -> forall e, dterm a1 e = dterm a2 e.
proof: Proof. induction 1; simpl; intros. - rewrite dterm_subst1; auto. - destruct b; auto. - rewrite IHred; auto. - rewrite IHred; auto. - rewrite IHred; auto. Qed.
imports: Coq(Bool String List Program.Equality) CDF(Sequences)