proposition: Lemma iters_aux_incl n ps : incl (snd ps) (fst ps) -> incl (snd (iters_aux n ps)) (fst (iters_aux n ps)).
proof: Proof. revert ps; elim n; simpl; auto; clear n. intros n Hrec (ss1, ss2) Hi; apply Hrec. apply (fold_nexts_incl (ss1, ss2)); auto with datatypes. intros z HH; inversion HH. Qed.
imports: ZArith List