proposition: Lemma fold_next2s_incl p ps ss : (forall s1, In s1 ss -> In s1 (fst (fst ps)) \/ In s1 (snd (fst ps))) -> (forall s1, In s1 (snd (fold_left (next2s p) (snd ps) (fst ps, ss))) -> In s1 (fst (fst (fold_left (next2s p) (snd ps) (fst ps, ss)))) \/ In s1 (snd (fst (fold_left (next2s p) (snd ps) (fst ps, ss))))).
proof: Proof. destruct ps as (ss1, ss2); simpl fst; simpl snd. revert ss1 ss; elim ss2; clear ss2; auto. intros s ss2 Hrec ss1 ss H1. repeat rewrite fold_left_cons. generalize (next2s_incl p (ss1, ss) s); case next2s. simpl fst; simpl snd. intros ss3 ss4 H3; apply Hrec; auto with datatypes. Qed.
imports: ZArith List