proposition: Lemma lt_size_inhabited A (s : A -> Prop) i (LT : lt_size i s) : inhabited A.
proof: Proof. destruct LT as [[]]; ins; desf; lia. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt