fact: Definition chains_ord := (fun S1 S2:chains => Included (proj1_sig S1) (proj1_sig S2)).
imports: Classical ClassicalChoice Relation_Definitions Relation_Definitions_Implicit Ensembles EnsemblesImplicit ProofIrrelevance InverseImage EnsemblesSpec Quotients EnsemblesSpec