proposition: Lemma equi_trans: forall x y z, x == y -> y == z -> x == z.
proof: Proof. cofix COINDHYP; intros x y z E1 E2; inversion E1; subst. - apply equi_terminates with v. auto. apply terminates_equi with y; auto. - inversion E2; subst. + inversion H0; subst. apply equi_terminates with v; auto. constructor. apply terminates_equi with y0; auto using equi_sym. + constructor. apply COINDHYP with y0; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List) CDF(Sequences IMP)