proposition: Lemma denot_some: forall n c s s', cinterp n c s = Some s' -> denot c s = Some s'.
proof: Proof. intros. apply denot_unique with n. intros. destruct (cinterp_mono n j c s H0); congruence. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)