proposition: Lemma LAppend_of_Infinite_eq (A:Type) : forall (u:LList A), Infinite u -> forall v:LList A, bisimilar u (LAppend u v).
proof: Proof. cofix H. simple destruct u. - inversion 1. - intros; autorewrite with llists using auto with llists. right; apply H; now apply Infinite_of_LCons with a. Qed.
imports: Arith List RelationClasses