I've often find myself needing to record a side condition before applying a lemma, like in the following context:

```
Γ: list context_decl
n: nat
d: context_decl
cl: is_closed_context Γ
=====================
nth_error Γ n = Some d -> ws_decl Γ (lift_decl (S n) 0 d)
```

I'd like to apply a lemma (using `move/`

) that uses my hypothesis cl and consumes the first hypothesis, but latter I need the fact that `n < #|Gamma|`

. I always first introduce the `nth`

hypothesis and add an appropriate `have lenGamman`

lemma to complete my proof, but I feel there must be a simpler way to just enrich the goal with any result that follows from the first hypothesis `nth_error Γ n = Some d`

In the current version of mathcomp, you can use `/[dup]`

to duplicate the top assumption.

```
Goal forall (A B C: Prop), (A -> B) -> A -> (A -> B -> C) -> C.
Proof. move=> A B C AB /[dup] /AB b a. by apply. Qed.
```

Cool, thanks!

And dup can easily be defined as:

Notation "[dup]" := (ltac:(let H := fresh in (move=> H; generalize H; move: H))).

These are actually in Coq 8.13 but you can "backport" the thing easily since "tactics as view" were added to SSR in Coq 8.10

@Cyril Cohen added them to mathcomp first, and ported them to Coq for 8.13

I meant, you can run last mathcomp on any "recent" Coq, or no mathcomp and Coq 8.13. (or backport it yourself, as you found out)

Last updated: Jul 15 2024 at 20:02 UTC