Hi! I am very new to Coq and I’m trying to prove a simple matrix transpose function. As part of my matrix transpose, I have a function called `maphd`

, which takes the head of each item in a list of lists, and returns the result as a new list.

I have:

```
Fixpoint maphd (l: list (list A)): (list A):=
match l with
| nil => nil
| a :: t => (hd a):: (maphd t)
end.
```

However, this fails with the error:

```
In environment
A : Type
maphd : list (list A) -> list A
l : list (list A)
a : list A
t : list (list A)
The term "maphd t" has type "list A"
while it is expected to have type "list (list (list A) -> list A)".
```

I don’t know how to put this right!