Mapping finite lists to lazy lists

Build an injection from list A into LList A. You must prove that your mapping is injective.

Resources

Here's the definition of type LList. 
Set Implicit Arguments.

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

Implicit Arguments LNil [A].

Solution

Follow this link

Going home
Pierre Castéran