How to apply hypothesis with a disjunction?

[jeffhappily]

Hi, I’m trying to proof a theorem, and here’s what I got.

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?

[LessnessR]

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.

[nojb]

Hello,

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

Best wishes,
Nicolás

[jeffhappily]

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