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