# 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.
## Solution

Follow this link

Going home

Pierre Castéran