proposition: Lemma desc_prefix : forall (x : List) (a : A), Descl (x ++ [a]) -> Descl x.
proof: Proof. intros. inversion H. - apply app_cons_not_nil in H1 as []. - assert (x ++ [a] = [x0]) by auto with sets. apply app_eq_unit in H0 as [(->, _)| (_, [=])]. auto using d_nil. - apply app_inj_tail in H0 as (<-, _). assumption. Qed.
imports: List Relation_Operators Operators_Properties Transitive_Closure