1) Prove that (∀cs | cs is finite) putCharList cs = map putChar cs

where

putCharList [] = []
putCharList (c:cs) = putChar c : putCharList cs

map f [] = []
map f (x:xs) = f x : map f xs

Base case:

putCharList []
  => []
  => map putChar []

Inductive Step:

assume that purCharList cs = map putChar cs

then

putCharList (c:cs)
  => putChar c : putCharList cs
  => putChar c : map putChar cs
  => map putChar (c:cs)

QED.

2) Prove that (∀xs | xs is finite) listProd xs = fold (*) 1 xs

where

listProd [] = 1
listProd (x:xs) = x * listProd xs

fold op init [] = init
fold op init (x:xs) = x `op` fold op init xs

Base case:

listProd []
  => 1
  => fold (*) 1 []

Inductive Step:

assume that listProd xs = fold (*) 1 xs

then

listProd (x:xs)
  => x * listProd xs
  => x * fold (*) 1 xs
  => fold (*) 1 (x:xs)

QED.