proposition: Theorem bisimilar_of_Infinite_is_Infinite (A:Type): forall l:LList A, Infinite l -> forall l':LList A, bisimilar l l' -> Infinite l'.
proof: Proof. cofix H. simple destruct l. - intro H0; inversion H0. - simple destruct l'. + inversion 1. + split; apply H with l0. * apply Infinite_of_LCons with a; assumption. * inversion H1; auto. Qed.
imports: Arith List RelationClasses