fact: Definition lt_size A i (s : A -> Prop) := exists dom, NoDup dom /\ (forall x, In x dom -> s x) /\ i < length dom.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt