proposition: Lemma fold_nexts_incl ps ss : incl ss (fst ps) -> incl (snd (fold_left nexts (snd ps) (fst ps, ss))) (fst (fold_left nexts (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 (nexts_incl (ss1, ss) s); case nexts. simpl fst; simpl snd. intros ss3 ss4 H3; apply Hrec; auto with datatypes. Qed.
imports: ZArith List