proposition: Lemma iters_aux_equiv n ps1 ps2 : pequiv ps1 ps2 -> pequiv (iters_aux n ps1) (iters_aux n ps2).
proof: Proof. revert ps1 ps2; elim n; simpl; auto; clear n. intros n Hrec (sl1, sr1) (sl2, sr2) H1. apply Hrec. apply (fold_nexts_equiv (sl1, sr1) (sl2, sr2)); auto. intros s; split; intros H; case H. Qed.
imports: ZArith List