proposition: Lemma next2s_incl p ps s : (forall s1, In s1 (snd ps) -> In s1 (fst (fst ps)) \/ In s1 (snd (fst ps))) -> (forall s1, In s1 (snd (next2s p ps s)) -> In s1 (fst (fst (next2s p ps s))) \/ In s1 (snd (fst (next2s p ps s)))).
proof: Proof. unfold next2s. match goal with |- context[fold_left ?X _ _] => change X with (fun ps f => let s1 := f s in filter2s p ps s1) end. generalize ps s; elim movel; auto; clear ps s. intros f lf Hrec ps s Hs; repeat rewrite fold_left_cons. generalize (filter2s_incl p ps (f s)). lazy zeta. case filter2s; intros (ss3, ss4) ss5 Hss3. apply Hrec; auto with datatypes; clear Hrec. Qed.
imports: ZArith List