proposition: Lemma restrict_well_ordered b X (wo: well_ordered X): well_ordered (restrict b X).
proof: Proof. firstorder. Qed.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)