A boggy definition of Infinity

Consider the following type:
Set Implicit Arguments.

CoInductive LList (A:Set) : Set :=
  | LNil : LList A
  | LCons : A -> LList A -> LList A.

Implicit Arguments LNil [A].
A distracted student confuses keywords and gives an inductive definition of being infinite:
Inductive BugInfinite (A:Set) : LList A -> Prop :=
    BugInfinite_intro :
      forall a (l:LList A),
        BugInfinite l -> BugInfinite (LCons a l).      
Show that this predicate can never be satisfied.


Follow this link

Going home
Pierre Castéran