Set Implicit Arguments. CoInductive LList (A:Set) : Set := | LNil : LList A | LCons : A -> LList A -> LList A. Implicit Arguments LNil [A].