proposition: Lemma to_listset_preserves_in x X : x ∈ to_listset X ↔ x ∈ X.
proof: Proof. Proof preserves_in id x X. Lemma fset_induction (P : set_type A → Prop) `{proper : !Proper ((=) ==> iff) P} : P ∅ → (∀ x X, x ∉ X → P X → P ({{ x }} ⊔ X)) → ∀ X, P X. Proof. intros Pempty Padd X. mc_setoid_replace X with (from_listset (to_listset X)) by (symmetry; apply (jections.bijective_applied _)). generalize (to_listset X). apply listset_induction. solve_proper. now rewrite preserves_bottom. intros x l E1 E2. change (P (fset_map id ({{x}} ⊔ l))). rewrite preserves_join, <-(fset_map_correct_applied _ x). apply Padd; auto. intros E3. destruct E1. now apply (preserves_in id x). Qed.
imports: MathClasses.theory.lattices MathClasses.varieties.monoids MathClasses.implementations.bool MathClasses.implementations.list_finite_set MathClasses.orders.lattices MathClasses.interfaces.abstract_algebra MathClasses.interfaces.finite_sets MathClasses.interfaces.orders