proposition: Lemma listset_add_raw_InA (l : list A) (x y : A) : y ∈ listset_add_raw x l → y = x ∨ y ∈ l.
proof: Proof. unfold contains, listset_in_raw. induction l; simpl. intros E. inversion_clear E; auto. case (decide_rel _); auto; intros E1 E2. inversion_clear E2; intuition. Qed.
imports: Coq.Lists.List Coq.Lists.SetoidList MathClasses.implementations.list MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders MathClasses.theory.lattices MathClasses.orders.lattices