proposition: Lemma Lappend_of_Infinite_0 (A:Type) : forall u:LList A, Infinite u -> forall v:LList A, u = LAppend u v.
proof: Proof. simple destruct u. - intro H; inversion H. - intros a l H; inversion H; intros. rewrite LAppend_LCons. assert (l = LAppend l v). Abort. CoInductive bisimilar (A:Type) : LList A -> LList A -> Prop := | bisim0 : bisimilar LNil LNil | bisim1 : forall (a:A) (l l':LList A), bisimilar l l' -> bisimilar (LCons a l) (LCons a l'). #[export] Hint Constructors bisimilar: llists. Lemma bisimilar_inv_1 (A:Type) : forall (a a':A) (u u':LList A), bisimilar (LCons a u) (LCons a' u') -> a = a'. Proof. intros a a' u u' H; now inversion H. Qed.
imports: Arith List RelationClasses