fact: Record well_order (R:relation T) : Prop := { wo_well_founded: well_founded R; wo_total_strict_order: total_strict_order R }.
imports: Relation_Definitions Relation_Definitions_Implicit Classical_Wf Description FunctionalExtensionality Classical ZornsLemma ProofIrrelevance EnsemblesSpec