test.v

Require Import ZArith.


  Inductive PrimValue :=
    | pBool (b: bool): PrimValue
    | pZ (n: Z) : PrimValue.

  Definition type_of (v: PrimValue): Type :=
    match v with
      | pBool _ => bool
      | pZ _ => Z
    end.

  Definition extract_value (v: PrimValue): type_of (v) :=
    match v with
      | pBool b => b
      | pZ i => i
    end.

  Definition extract_valueT (v: PrimValue)
                            (T: Type)
                            (H: type_of v = T): T.
    intros; destruct v; simpl in *; rewrite <- H.
      exact b. exact n. Qed.


  Definition extract_valueT' (v: PrimValue)
                             (T: Type)
                             (H: type_of v = T) : T :=
    match v in ??? return ??? with
    | ???
    end.