[TYPES] Proof term for proof by exhaustion

[Param Jyothi Reddy]

Hi,
Lets define vector in usual way with constructors:
nil : Vector T 0
cons : Vector T n -> T -> Vector T (S n)

along with its inductive elimination rule. Let BD be type of Binary
Digits (enumeration with elements 0 and 1).

Also lets say i have proofs of some predicate P for all elements of
Vector's over BD of length 2, i.e.

p_0 : P(00), p_1 : P(01), p_2 : P(10), p_3 : P(11), where bd is cons
(cons nil d) b.

using these How will the proof term for

(forall v : Vector BD (S S 0) ). P(v) look like?


I can use or elimination if i could build proof for:

(forall v : Vector BD (S S 0)). v == 00 or v == 01 or v == 10 or v ==
11. However i am not sure how the proof term for this looks either.

Can someone help me understand this?

Thanks,
Param