proposition: Lemma denot_seq: forall c1 c2 s, denot (SEQ c1 c2) s = bind (denot c1 s) (denot c2).
proof: Proof. intros. unfold bind. destruct (denot_charact c1 s) as (i1 & LIM1). destruct (denot c1 s) as [s1|] eqn:D1. - destruct (denot_charact c2 s1) as (i2 & LIM2). apply denot_unique with (S (Nat.max i1 i2)); intros. destruct j as [ | j]. lia. cbn. unfold bind. rewrite LIM1, LIM2 by lia. auto. - apply denot_none. intros. destruct n; cbn; auto. destruct (denot_eq c1 s n) as [E|E]; rewrite E, ?D1; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)