Как конвертировать natlist в natprod

Question

У меня есть natlist и я хочу преобразовать его в natprod p = (fst p, snd p) таким образом, чтобы первый элемент natlist дал fst p, а последний элемент * snd p. Спасибо за помощь.

Fixpoint fs (l:natlist) :(fst p, snd p)  :=
  match l with
  | nil => (nil,nil)
  | h :: t => fst p(h)  match t with
                        |o => snd p
                        |t+1 =>snd p
                        end
   end.