proposition: Lemma countable_subset s s' : countable s' -> s ⊆₁ s' -> countable s.
proof: Proof. unfold countable at 1; ins; desf; vauto. pose proof (enumerates_surjection H). eapply surjection_countable with (f := nu); eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt