proposition: Lemma left_prefix : forall x y z:List, ltl (x ++ y) z -> ltl x z.
proof: Proof. simple induction x. simple induction z. simpl; intros H. inversion_clear H. simpl; intros; apply (Lt_nil A leA). intros a l HInd. simpl. intros. inversion_clear H. apply (Lt_hd A leA); auto with sets. apply (Lt_tl A leA). apply (HInd y y0); auto with sets. Qed.
imports: Coq(List Relation_Operators Transitive_Closure)