A boggy definition of Infinity

Consider the following declarations:

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

Arguments LNil {A}.
Arguments LCons {A} _ _.

A distracted student confuses keywords and gives an inductive definition of being infinite:

Inductive BugInfinite {A: Type} : LList A -> Prop :=
    BugInfinite_intro :
      forall a (l:LList A),
        BugInfinite l -> BugInfinite (LCons a l).

Show that this predicate can never be satisfied.

Solution

Follow this link