proposition: Lemma filter_InA : forall f, Proper (eqA==>eq) f -> forall l x, InA x (List.filter f l) <-> InA x l /\ f x = true.
proof: Proof. clear sotrans ltA ltA_strorder ltA_compat. intros f H l x; do 2 rewrite InA_alt; intuition; match goal with Hex' : exists _, _ |- _ => rename Hex' into Hex end. - destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; exists y; intuition. - destruct Hex as (y,(H0,H1)); rewrite filter_In in H1; intuition. rewrite (H _ _ H0); auto. - destruct Hex as (y,(H0,H1)); exists y; rewrite filter_In; intuition. rewrite <- (H _ _ H0); auto. Qed.
imports: List Sorted Setoid Basics Morphisms