proposition: Lemma dist_Desc_concat : forall x y : List, Descl (x ++ y) -> Descl x /\ Descl y.
proof: Proof. intros. apply (dist_aux (x ++ y) H x y); auto with sets. Qed.
imports: List Relation_Operators Operators_Properties Transitive_Closure