proposition: Theorem LAppend_of_Finite (A:Type): forall (l l':LList A), Finite l -> Finite l' -> Finite (LAppend l l').
proof: Proof. intros l l' H; induction H; autorewrite with llists using auto with llists. Qed.
imports: Arith List RelationClasses