proposition: Lemma enumerates_surjection (s : A -> Prop) nu (E : enumerates nu s) : forall a (IN: s a), exists i, nu i = a.
proof: Proof. unfold enumerates in *; desf; ins. specialize_full SUR; eauto; desf; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt