How to apply hypothesis with a disjunction?

Hi, I’m trying to proof a theorem, and here’s what I got.
Screenshot from 2020-05-08 16-13-25

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?

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.

1 Like


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

Best wishes,

1 Like

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