proposition: Lemma listset_induction (P : set_type A → Prop) `{proper : !Proper ((=) ==> iff) P} : P ∅ → (∀ x l, x ∉ l → P l → P ({{ x }} ⊔ l)) → ∀ l, P l.
proof: Proof. intros Pempty Padd. intros [l Pl]. induction l as [|x l]. apply proper with ∅; firstorder. inversion_clear Pl as [|??? Pl']. apply proper with ({{ x }} ⊔ l↾Pl'); auto. intros z. change (z ∈ x :: l ↔ z ∈ listset_add_raw x l). now rewrite listset_add_raw_cons. 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