proposition: Lemma LAppend_G_Infinite (P:LList A -> Prop): forall (u v:LList A) , Finite u -> satisfies v (G_Infinite P) -> satisfies (LAppend u v) (G_Infinite P).
proof: Proof. simple induction 1. - autorewrite with llists using auto. - intros a0 l H0 H1; autorewrite with llists using auto. right; now apply H1. Qed.
imports: Arith List RelationClasses