proposition: Lemma countable_ext A (s : A -> Prop) (C: countable s) (r : relation A) (PO : strict_partial_order r) (F : fsupp r) : ~ inhabited A \/ exists f, enumerates f s /\ forall i j (Li : lt_size i s) (Lj: lt_size j s) (R: r (f i) (f j)), i < j.
proof: Proof. destruct C; desf; eauto using enum_ext. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt