proposition: Lemma filter2s_valid p ps s1 : valid_triple ps -> valid_state s1 -> valid_triple (filter2s p ps s1).
proof: Proof. destruct ps as ((ss1, ss2), ss3). intros ((Hg1, Hg2), Hg3) Hg; repeat split; intros s; simpl in Hg1, Hg2, Hg3; unfold filter2s; case in_states; simpl; auto; case in_states; simpl; auto; (case p; [intros p1 | intros p1 | idtac]); simpl; auto with datatypes; intros [H1 | H1]; auto; subst s1; auto. Qed.
imports: ZArith List