proposition: Lemma iter2s_incl n : (forall s1, In s1 (snd (iter2s n)) -> In s1 (fst (fst (iter2s n))) \/ In s1 (snd (fst (iter2s n)))).
proof: Proof. unfold iter2s; apply iter2s_aux_incl; simpl; auto with datatypes. Qed.
imports: ZArith List