# How to apply hypothesis with a disjunction?

**URL:** <https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832>\
**Category:** Using Rocq\
**Created:** [May 8, 2020, 8:22am UTC](https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832 "2020-05-08T08:22:52Z")\
**Posts on this page:** 4\
**Page:** 1

<div class="post-metadata">

**Author:** ![jeffhappily](https://avatars.discourse-cdn.com/v4/letter/j/85e7bf/32.png) [@jeffhappily](https://discourse.rocq-prover.org/u/jeffhappily)\
**Post date:** [May 8, 2020, 8:22am UTC](https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832/1 "2020-05-08T08:22:53Z")

</div>

Hi, I’m trying to proof a theorem, and here’s what I got.  
 ![Screenshot from 2020-05-08 16-13-25](https://us1.discourse-cdn.com/flex001/uploads/coq/original/1X/3574c81bdced0c59a1cd1a713c0ab4539842cc5f.png)

I’m trying to apply H0 to H5 by using `apply H0 in H5` but it doesn’t seem to work, if H0 is just simply  
`forall x0 : X, In x0 l1' -> In x0 l2` then it should work. But I don’t know how to get it working with the disjuction. Can anyone help with this?

---

<div class="post-metadata">

**Author:** ![LessnessR](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lessnessr/32/783_2.png) [@LessnessR](https://discourse.rocq-prover.org/u/LessnessR)\
**Post date:** [May 8, 2020, 8:34am UTC](https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832/2 "2020-05-08T08:34:16Z")

</div>

This works

```
pose proof (H0 y (or_intror H5)).

```

Or maybe

```
assert (In y l2) by (apply H0; auto).

```

I believe it’s impossible to do it more directly. If I’m wrong, I’m interested in the solution too.

---

<div class="post-metadata">

**Author:** ![nojb](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/nojb/32/256_2.png) [@nojb](https://discourse.rocq-prover.org/u/nojb)\
**Post date:** [May 8, 2020, 9:25am UTC](https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832/3 "2020-05-08T09:25:18Z")

</div>

Hello,

You can also do `specialize (H0 _ (or_introl H5))` to replace `H0` in place by its conclusion.

Best wishes,  
Nicolás

---

<div class="post-metadata">

**Author:** ![jeffhappily](https://avatars.discourse-cdn.com/v4/letter/j/85e7bf/32.png) [@jeffhappily](https://discourse.rocq-prover.org/u/jeffhappily)\
**Post date:** [May 8, 2020, 9:28am UTC](https://discourse.rocq-prover.org/t/how-to-apply-hypothesis-with-a-disjunction/832/4 "2020-05-08T09:28:28Z")

</div>

Thanks for being so helpful guys! I’ve got it working!