proposition: Lemma dist_aux : forall z : List, Descl z -> forall x y : List, z = x ++ y -> Descl x /\ Descl y.
proof: Proof. intros z D. induction D as [| | * H D Hind]; intros. - assert (H0 : x ++ y = []) by auto with sets. apply app_eq_nil in H0 as (->, ->). split; apply d_nil. - assert (E : x0 ++ y = [x]) by auto with sets. apply app_eq_unit in E as [(->, ->)| (->, ->)]. + split. * apply d_nil. * apply d_one. + split. * apply d_one. * apply d_nil. - induction y0 using rev_ind in x0, H0 |- *. + rewrite app_nil_r in H0. rewrite <- H0. split. * apply d_conc; auto with sets. * apply d_nil. + induction y0 using rev_ind in x1, x0, H0 |- *. * simpl. split. -- apply app_inj_tail in H0 as (<-, _). assumption. -- apply d_one. * rewrite 2!app_assoc in H0. apply app_inj_tail in H0 as (H0, <-). pose proof H0 as H0'. apply app_inj_tail in H0' as (_, ->). rewrite <- app_assoc in H0. apply Hind in H0 as []. split. -- assumption. -- apply d_conc; auto with sets. Qed.
imports: List Relation_Operators Operators_Properties Transitive_Closure