proposition: Lemma iter2s_aux_incl n p ps : (forall s1, In s1 (snd ps) -> In s1 (fst (fst ps)) \/ In s1 (snd (fst ps))) -> (forall s1, In s1 (snd (iter2s_aux n p ps)) -> In s1 (fst (fst (iter2s_aux n p ps))) \/ In s1 (snd (fst (iter2s_aux n p ps)))).
proof: Proof. revert p ps; elim n; simpl; auto; clear n. intros n Hrec p (ss1, ss2) Hi; apply Hrec. apply (fold_next2s_incl p (ss1, ss2)); auto with datatypes. intros z HH; inversion HH. Qed.
imports: ZArith List