proposition: Lemma filters_valid ps s1 : valid_pair ps -> valid_state s1 -> valid_pair (filters ps s1).
proof: Proof. destruct ps as (ss1, ss2); intros (Hg1, Hg2) Hg; split; intros s; unfold filters; case in_states; simpl; auto; intros [H1 | H1]; auto; subst s1; auto. Qed.
imports: ZArith List