proposition: Lemma denot_charact: forall c s, exists i, forall j, i <= j -> cinterp j c s = denot c s.
proof: Proof. intros. apply limit_charact. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)