proposition: Lemma LAppend_G_Infinite_R (P:LList A -> Prop): forall (u v:LList A) , Finite u -> satisfies (LAppend u v) (G_Infinite P) -> satisfies v (G_Infinite P).
proof: Proof. simple induction 1. - autorewrite with llists using auto. - intros a0 l H0 H1 H2; autorewrite with llists using auto. rewrite LAppend_LCons in H2; inversion_clear H2. + apply H1. inversion_clear H3. generalize H4; case (LAppend l v). * inversion 1. * left; auto. + auto. Qed.
imports: Arith List RelationClasses