proposition: Lemma diag_nth `(v : vector (vector A n) n) (f : fin n) : nth (diag v) f = nth (nth v f) f.
proof: Proof. revert f. funelim (diag v); intros f. depelim f. depelim f; simp nth; trivial. rewrite H. now simp nth. Qed.
imports: Program Bvector List Relations Equations(Equations Signature) Utf8 Arith Wf_nat Bvector Examples.Fin