proposition: Lemma terminates_equi: forall x v, terminates x v -> forall y, x == y -> terminates y v.
proof: Proof. induction 1; intros y E; inversion E; subst. - inversion H; auto. - inversion H0; subst. assert (v0 = v) by (eapply terminates_unique; eauto). subst v0; auto. - constructor; eauto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)