I’d like to pass a proof that `n > 0`

into `hd`

because the type signature `t A (S n) -> A`

is causing me issues and I have a spare proof of my `n > 0`

lying around.

I’ve been experimenting with filling out `Definitions`

by writing proofs instead of specifying the combinator, because another function I wrote *only* worked that way for reasons I’ll tell you another time. But this seems to have gone well:

```
Definition hd_proof {A : Type} {n : nat} (v : t A n) (H : n > 0) : A.
Proof.
induction n; try lia.
remember (hd v) as x.
simpl in x.
apply x.
Qed.
```

My understanding is that the proof script is manipulating and ultimately creating a *proof object*, which is a sort of combinator. So I figured it would apply.

```
Lemma fourgtone : 4 > 0. Proof. lia. Qed.
Compute hd_proof [1;2;3;4] fourgtone.
(* response:
= hd_proof [1; 2; 3; 4] fourgtone
: nat
*)
```

Can I Make `Compute`

actually compute and terminate at `1`

?