proposition: Lemma general_omega_lappend (A:Type): forall (u v:LList A), bisimilar (general_omega v u) (LAppend v (omega u)).
proof: Proof. cofix H. simple destruct v. - autorewrite with llists using auto with llists. rewrite general_omega_shoots_again. unfold omega in |- *; auto with llists. intros; autorewrite with llists using auto with llists. reflexivity. - intros; autorewrite with llists using auto with llists. Qed.
imports: Arith List RelationClasses