proposition: Theorem bisimilar_of_Finite_is_eq (A: Type) : forall l:LList A, Finite l -> forall l':LList A, bisimilar l l' -> l = l'.
proof: Proof. simple induction 1. - intros l' H1; inversion H1; auto. - simple destruct l'. + inversion 1. + intros a0 l1 H2; inversion H2; auto with llists. rewrite (H1 l1); auto. Qed.
imports: Arith List RelationClasses