proposition: Lemma bisimilar_LNth (A:Type): forall (n:nat) (u v:LList A), bisimilar u v -> LNth n u = LNth n v.
proof: Proof. simple induction n; simple destruct u; simple destruct v. - intros; cbn in |- *; trivial. - intros a l H; inversion H. - intro H; inversion H. - intros a0 l0 H; inversion H; cbn in |- *; trivial. - intros; cbn in |- *; trivial. - intros a l H0; inversion H0. - intro H0; inversion H0. - cbn in |- *; auto. intros a0 l0 H0; inversion_clear H0; auto. Qed.
imports: Arith List RelationClasses