proposition: Lemma LAppend_of_Infinite (A:Type) : forall u:LList A, Infinite u -> forall v:LList A, Infinite (LAppend u v).
proof: Proof. cofix H. - simple destruct u. + inversion 1. + intros a l H0 v. autorewrite with llists using auto with llists. split; apply H; inversion H0; auto. Qed.
imports: Arith List RelationClasses