proposition: Lemma elem_of_list_In {A} (l : list A) x : x ∈ l ↔ In x l.
proof: Proof. split. - induction 1; simpl; auto. - induction l; destruct 1; subst; constructor; auto. Qed.
imports: Coq(Permutation) Coq.ssr((notations) ssrfun) stdpp(options)