If I have a goal of type `nat`

, and I want to derive through typeclass resolution an instance of `ThisNat n`

where `ThisNat`

is a class and `n`

a concrete nat, then use `n`

to prove the goal.

Is there a way to do that using Ltac so that the resulting proof term is exactly `n`

, without any trace of the type class resolution or trace of `ThisNat`

?

```
Class Foo (n : nat).
Instance xxx : Foo 3. Defined.
Definition ooF n (_ : Foo n) := n.
Goal nat.
let solution := eval cbv in (ooF _ _) in exact solution.
Show Proof.
```

Right. I guess I wanted to avoid `ooF`

appearing in the proof term. But now I'm not sure it's very important

Ah wait nvm, didn't see the second part

thanks!

Last updated: Sep 26 2023 at 12:02 UTC