proposition: Lemma filter2s_incl p ps s : (forall s1, In s1 (snd ps) -> In s1 (fst (fst ps)) \/ In s1 (snd (fst ps))) -> (forall s1, In s1 (snd (filter2s p ps s)) -> In s1 (fst (fst (filter2s p ps s))) \/ In s1 (snd (fst (filter2s p ps s)))).
proof: Proof. destruct ps as ((ss1, ss2), ss3). intro H; unfold filter2s; intros s1. do 2 (case in_states; simpl; auto with datatypes); case p; [intros p1 | intros p1 | idtac]; simpl in H |- *; intros [H1 | H1]; subst; auto; case (H _ H1); auto. Qed.
imports: ZArith List