proposition: Lemma countable_downward_closed {X : Type} (S T : Ensemble X) : Countable T -> Included S T -> Countable S.
proof: Proof. intros [f H] H0. exists (fun x => match x with | exist x0 i => f (exist _ x0 (H0 _ i)) end). intros [x1] [x2] H1. apply H in H1. injection H1 as H1. destruct H1. now apply subset_eq. Qed.
imports: Coq(Arith ArithRing ClassicalChoice Description FunctionalExtensionality Lia Relation_Definitions Program.Subset QArith ZArith) ZornsLemma(CSB DecidableDec DependentTypeChoice Finite_sets FiniteTypes FunctionPropertiesEns IndexedFamilies InfiniteTypes)