list - 空でないリストのコモナド

Question

私はコモナドについて熟考してきましたが、空でないリスト (「完全なリスト」) はコモナドであるという直感を持っています。私は Idris で妥当な実装を構築し、共通法則の証明に取り組みましたが、いずれかの法則の再帰分岐を証明することはできませんでした。これ（穴）を証明するにはどうすればよいですか？?i_do_not_know_how_to_prove_this_if_its_provableまたは、私の実装が有効なコモナドであることについて間違っていますか（HaskellのNonEmptyコモナド実装を見てきましたが、私のものと同じようです）？

module FullList

%default total

data FullList : Type -> Type where
  Single : a -> FullList a
  Cons : a -> FullList a -> FullList a

extract : FullList a -> a
extract (Single x) = x
extract (Cons x _) = x

duplicate : FullList a -> FullList (FullList a)
duplicate = Single 

extend : (FullList a -> b) -> FullList a -> FullList b
extend f (Single x) = Single (f (Single x))
extend f (Cons x y) = Cons (f (Cons x y)) (extend f y)

extend_and_extract_are_inverse : (l : FullList a) -> extend FullList.extract l = l
extend_and_extract_are_inverse (Single x) = Refl
extend_and_extract_are_inverse (Cons x y) = rewrite extend_and_extract_are_inverse y in Refl

comonad_law_1 : (l : FullList a) -> extract (FullList.extend f l) = f l
comonad_law_1 (Single x) = Refl
comonad_law_1 (Cons x y) = Refl

nesting_extend : (l : FullList a) -> extend f (extend g l) = extend (\x => f (extend g x)) l
nesting_extend (Single x) = Refl
nesting_extend (Cons x y) = ?i_do_not_know_how_to_prove_this_if_its_provable