proposition: Lemma bind_context: forall (A B: Type) (m1 m2: delay A) (f1 f2: A -> delay B), m1 == m2 -> (forall v, f1 v == f2 v) -> bind m1 f1 == bind m2 f2.
proof: Proof. cofix CIH; intros. inversion H; subst. - apply equi_trans with (f1 v). apply bind_terminates_l; auto. apply equi_trans with (f2 v). auto. apply equi_sym. apply bind_terminates_l; auto. - rewrite ! bind_later. constructor. apply CIH; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)