proposition: Lemma denot_seq: forall c1 c2 s, denot (SEQ c1 c2) s == bind (denot c1 s) (denot c2).
proof: Proof. unfold denot; intros. rewrite (u_mon (cinterp (c1;;c2) s)); cbn. apply run_Bind. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)