proposition: Lemma filters_incl ps s : incl (snd ps) (fst ps) -> incl (snd (filters ps s)) (fst (filters ps s)).
proof: Proof. destruct ps as (ss1, ss2); intro H; unfold filters. case in_states; simpl; auto with datatypes. Qed.
imports: ZArith List