proposition: Lemma in_prefixes a b : In a (prefixes b) <-> r a b.
proof: Proof. unfold prefixes; rewrite in_isort_iff, in_undup_iff; in_simp; intuition. destruct (constructive_indefinite_description _ (F b)); ins; eauto. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt