The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

frank maltman wrote:
> I understand the correct thing to do is to use a proof of False
> to create a value of any type in order to satisfy the type
> checker (I realize I could also just return any one of the other
> fields, but I'd rather not!).
>    

Yup, and here's one way of doing so:

Definition get {A : Set} (f : finite 4) (c : contrived A) : A :=
  match c with
    | C n0 n1 n2 n3 =>
      match finite_nat f as n return n < 4 -> A with
        | 0 => fun _ => n0
        | 1 => fun _ => n1
        | 2 => fun _ => n2
        | 3 => fun _ => n3
        | _ => fun pf => match lt_SSSSn_4_absurd _ pf with end
      end (lt_finite_nat_fb_b _ _)
  end.