rewriting hypothesis to false with a contradictory theorem

Question

I want to show that

[seq q x t | x <- iota 0 (t + 1)] != [::]

I decided to destruct iota 0 (t + 1) because I have a lemma that says:

iota 0 (t + 1) != [::]

So the first case of destruct should have iota 0 (t + 1) = [::] which by the theorem mentioned is false, and I can discriminate. How can I rewrite the equation in the first destruct case using the lemma? I cannot figure it out.

Thanks.

Answer 1

You do not need to destruct. Note that iota is defined by recursion on its second variable. Your current goal cannot be simplified because t + 1 does not start with a constructor. However, you can do by rewrite addn1 to put it in a form where it can be solved.