Hi there!
I am trying to prove the following theorem:
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!
Hi there!
I am trying to prove the following theorem:
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: