list is inductive type for sure, not coinductive. But it could be used for modelling infinite(but countable) sequences in the sense that following property bein

list is inductive type for sure, not coinductive. But it could be used for modelling infinite(but countable) sequences in the sense that following property being hold: forall (m:nat), exists (l: list nat), length l > m.