proposition: Lemma desc_prefix : forall (x:List) (a:A), Descl (x ++ Cons a Nil) -> Descl x.
proof: Proof. intros. inversion H. generalize (app_cons_not_nil _ _ _ H1); simple induction 1. cut (x ++ Cons a Nil = Cons x0 Nil); auto with sets. intro. generalize (app_eq_unit _ _ H0). simple induction 1; simple induction 1; intros. rewrite H4; auto using d_nil with sets. discriminate H5. generalize (app_inj_tail _ _ _ _ H0). simple induction 1; intros. rewrite <- H4; auto with sets. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)