# How to refer a hypothesis in an assert?

**URL:** <https://discourse.rocq-prover.org/t/how-to-refer-a-hypothesis-in-an-assert/2871>\
**Category:** Using Rocq\
**Created:** [December 7, 2025, 1:00pm UTC](https://discourse.rocq-prover.org/t/how-to-refer-a-hypothesis-in-an-assert/2871 "2025-12-07T13:00:27Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![shutterrecoil](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/shutterrecoil/32/1036_2.png) [@shutterrecoil](https://discourse.rocq-prover.org/u/shutterrecoil)\
**Post date:** [December 7, 2025, 1:00pm UTC](https://discourse.rocq-prover.org/t/how-to-refer-a-hypothesis-in-an-assert/2871/1 "2025-12-07T13:00:27Z")

</div>

Hi,

I would like to know how to reuse a hypothesis in an assert definition.

The hypothesis body is long and copy-pasting it is not efficient, so I tried to refer the required hypothesis by its name, but it turned out a different thing and Rocq prover rejects the same prop when it is referred.

command:

```auto
assert (NH: ~ H).

```

goals:

```auto
H: long-prop
============
False

```

response:

```auto
The term "H" has type "..." while it is expected to have type "Prop".

```

---

<div class="post-metadata">

**Author:** ![SkySkimmer](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/skyskimmer/32/369_2.png) [@SkySkimmer](https://discourse.rocq-prover.org/u/SkySkimmer)\
**Post date:** [December 7, 2025, 1:15pm UTC](https://discourse.rocq-prover.org/t/how-to-refer-a-hypothesis-in-an-assert/2871/2 "2025-12-07T13:15:38Z")

</div>

it seems like you want the type of the hypothesis, not the hypothesis itself  
so “let t := type of H in assert (NH: ~ t)”

Gaëtan Gilbert