proposition: Lemma LNth_bisimilar (A:Type) : forall u v:LList A, (forall n:nat, LNth n u = LNth n v) -> bisimilar u v.
proof: Proof. cofix H. simple destruct u; simple destruct v. - left. - intros a l H1; generalize (H1 0); discriminate 1. - intro H1; generalize (H1 0); discriminate 1. - intros a0 l0 H0; generalize (H0 0); cbn in |- *. injection 1; intro; subst a0; right. apply H; intro n; generalize (H0 (S n)); auto. Qed.
imports: Arith List RelationClasses