proposition: Lemma general_omega_of_Finite (A:Type) : forall u:LList A, Finite u -> forall v:LList A, general_omega u v = LAppend u (general_omega v v).
proof: Proof. simple induction 1. - intros; autorewrite with llists using auto with llists. now rewrite general_omega_shoots_again. - intros; autorewrite with llists using auto. rewrite H1; auto. Qed.
imports: Arith List RelationClasses