proposition: Lemma LAppend_assoc (A:Type): forall (u v w:LList A), bisimilar (LAppend u (LAppend v w)) (LAppend (LAppend u v) w).
proof: Proof. cofix H. simple destruct u; intros; autorewrite with llists using auto with llists. reflexivity. Qed.
imports: Arith List RelationClasses