Using finiteness hypotheses

Consider the following proof (from this file ):

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).

Build a counterexample for showing that the hypothesis Finite u is necessary.

Solution

Follow this link

Going home

Pierre Castéran