How to destruct H involving two variables

Hi there!

I am trying to prove the following theorem:
image

image

How do I destruct H to remove the “forall a1 a2” part so that I can try to use H? I am unable to figure out the syntax. Can someone help me out?

Thanks!

You can use specialize (H arg1 arg2). Or destruct (H arg1 arg2) if you want to destruct it.

Hi!

Thank you so much for your reply! I tried it out but am getting the following error:

image