proposition: Lemma decomp2 {A} : forall v : Vector.t A 2, v = [Vector.hd v; Vector.hd (Vector.tl v)].
proof: Proof. intro v; rewrite (decomp _ 1 v), (decomp _ _ (Vector.tl v)). simpl. rewrite (t_0_nil _ (Vector.tl (Vector.tl v))). reflexivity. Defined.