proposition: Lemma equi_sym: forall x y, x == y -> y == x.
proof: Proof. cofix COINDHYP; intros x y E; inversion E; subst. - apply equi_terminates with v; auto. - apply equi_later; apply COINDHYP; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)