proposition: Lemma filter_In' : ∀ (A : Type) (f : A → bool) (x : A) (l : list A), In x (filter f l) ↔ In x l ∧ f x.
proof: Proof. intros. rewrite filter_In. intuition auto. apply Is_true_eq_true2. auto. apply Is_true_eq_true. auto. Qed.
imports: Program Utf8 Equations.Prop.Equations Bvector List Relations Arith Wf_nat Lia Coq.Lists.SetoidList Coq.Sorting.Sorting Coq.Sorting.Permutation Coq.Sorting.PermutSetoid Bool EquivDec Permutation