proposition: Lemma denot_unique: forall c s i lim, (forall j, i <= j -> cinterp j c s = lim) -> denot c s = lim.
proof: Proof. intros. destruct (denot_charact c s) as (i' & LIM'). set (j := Nat.max i i'). rewrite <- (H j), <- (LIM' j) by lia. auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP Compil) Coq(Classical Description)