The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Tom Prince wrote:
> Axiom param : nat ->  Type.
> Axiom val : ∀ n, param n.
>
> [snip]
>
> Record rec := { m1 : param 0; m7: param 6; m6: param 5 }.
>
> Goal rec.
>    

I think the example is abstracted a bit too much to illustrate the 
issues, as [constructor; apply val] leads to the value of [rec] that 
you're looking for.  Can you give a more complicated example which shows 
what makes your real code trickier?

Someone might very well tell you how to abstract the argument to 
[constructor] (I feel like I've seen this before somewhere), but I have 
a feeling that a more fundamental reformulation of the problem would 
yield better results.