Hi!

I’ve been doing a lot of reading about tactics (and I cannot stress enough how much of a beginner I am at this), and I’m not sure how best to prove the following:

```
Program Fixpoint transp (l: list (list A)){measure (length l)}:list(list A) :=
match l with
| nil => nil
| nil :: t => transp t
| (a :: r) :: t => (a :: maphd t)::transp(r::maptl t)
end.
Next Obligation.
Admitted.
Next Obligation.
Admitted.
Theorem transptransp: forall a: list(list A),
a=transp (transp a).
Proof.
intros a.
unfold transp.
unfold maphd.
unfold maptl.
induction a as [| a' IHa'].
- (* a = 0 *)
simpl.
auto.
```

Is what I currently have (I can supply the maphd and maptl functions if necessary). I simply want to prove my transpose function by saying that transpose(transpose x) =x. Reflexivity doesn’t work; I clearly need to unpick my proof a bit more but I don’t know how!

Is it a problem that I cheated and used measure to convince the compiler that my recursion is well-founded?