proposition: Lemma listset_meet_raw_NoDupA (l k : list A) : NoDupA (=) l → NoDupA (=) (l ⊓ k).
proof: Proof. unfold meet. intros Pl. induction l; simpl; auto. inversion_clear Pl as [|? ? E1]. case (decide_rel); intros; auto. apply NoDupA_cons; auto. intros E2. destruct E1. now apply (listset_in_meet_raw l k _). 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