proposition: Lemma denot_eq: forall c s n, cinterp n c s = None \/ cinterp n c s = denot c s.
proof: Proof. intros. destruct (cinterp n c s) as [s'|] eqn:C; auto. right; symmetry; apply denot_some with n; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)