proposition: Lemma denot_none: forall c s, (forall n, cinterp n c s = None) <-> denot c s = None.
proof: Proof. intros; split; intros. - apply denot_unique with O. auto. - destruct (cinterp n c s) as [s'|] eqn:C; auto. apply denot_some in C. congruence. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)