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.