proposition: Lemma Eventually_of_LAppend : forall (P:LList A -> Prop) (u v:LList A), Finite u -> satisfies v (Eventually P) -> satisfies (LAppend u v) (Eventually P).
proof: Proof. unfold satisfies in |- *; simple induction 1; intros; autorewrite with llists using auto with llists. Qed.
imports: Arith List RelationClasses