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