proposition: Theorem bisimilar_of_Finite_is_Finite {A: Type} : forall l:LList A, Finite l -> forall l':LList A, bisimilar l l' -> Finite l'.
proof: Proof. simple induction 1. - simple destruct l'. + auto with llists. + inversion 1. - simple destruct l'. + inversion 1. + inversion 1; auto with llists. Qed.
imports: Arith List RelationClasses