proposition: Lemma terminates_unique: forall (A: Type) (x: delay A) (v1 v2: A), terminates x v1 -> terminates x v2 -> v1 = v2.
proof: Proof. intros until v2; intros T; revert x v1 T v2. induction 1; intros. - inversion H; subst; auto. - inversion H; subst; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)