A Coercion from vectors of length 2 to ordered pairs

First Question

Consider the following definitions:
Require Import Bvector.

Implicit Arguments Vcons [A n].
Implicit Arguments Vnil [A].
Implicit Arguments Vhead [A n].
Implicit Arguments Vtail [A n].

Definition vec2 (A:Type) := vector A 2.

Definition vcons2 (A:Type)(a b:A): vec2 A := Vcons a (Vcons b Vnil).
Implicit Arguments vcons2 [A].

Define a coercion from vec2 to the class prod of cartesian products. The following commands should work properly:
Check (fst (vcons2 3 4)). 

Eval compute in (snd (vcons2 3 4)).

A (more difficult) question

Prove the following theorem:
Lemma V2 : forall A (v:vec2 A), v= vcons2 (fst v) (snd v).

Hint The solution of the second question may use dependent elimination. Please refer to The tutorial on [Co]-Inductive Types in Coq (Section 6).

Solution

Look at this file .
Going home