I am still trying to understand Coq and working on a matrix transpose algorithm. I have refactored what I had before:

```
Require Import Ensembles.
Require Import ZArith.
Require Extraction.
Extraction Language Haskell.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.
From Coq Require Import List.
Notation "x :: l" := (cons x l)
(at level 60, right associativity).
Notation "[ x ; .. ; y ]" := (cons x .. (cons y nil) ..).
Definition vector := list.
Definition matrix A := list (vector A).
(*M = [ (v1) , (v2), (v3), ..., (vn) ]*)
Definition column A (M:matrix A) (i:nat) : list A := nth i M nil.
Fixpoint row A (M:matrix A) (i:nat) (bottom: A) : list A :=
match M with
| nil => nil
| v1::M => (nth i v1 bottom)::(row A M i bottom)
end.
Definition transp A (M:matrix A) (Mt:matrix A) :=
forall bottom, forall i,
column A M i = row A Mt i bottom /\
row A M i bottom = column A Mt i.
Theorem transp_transp_eq A M Mt Mtt:
transp A M Mt ->
transp A Mt Mtt ->
M = Mtt.
```

However, I don’t know how to discharge a proof about my theorem. I’ve tried a lot of different tactics, but I can’t exactly figure out what to do.

I have

```
Proof.
intros HMMt HMtMtt.
unfold transp.
induction M.
```

But I can’t even prove the nil case!