H: l1=[b] ( l:list nat,b:nat)
In goal statement ,i have pattern matching on l1,like this
match l1 with
First , apply induction on l1,then it become
statement is wrong because l1 cannot be empty,according to l1 it contains one element.How H can be helpful here?
You can do e.g.
inversion H1which splits the goal into all ways in which H1 could be valid - which are none
congruencewhich is a decision procedure for equalities
subst l1 or
rewrite H could work as well.
Last updated: Oct 04 2023 at 22:01 UTC