proposition: Lemma eq_later: forall x, later x == x.
proof: Proof. cofix COINDHYP; intros x. destruct x. - apply equi_terminates with a; repeat constructor. - apply equi_later. apply COINDHYP. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)