H: l1=[b] ( l:list nat,b:nat)

In goal statement ,i have pattern matching on l1,like this

match l1 with

| []=>false

| h::t=>true

end true.

First , apply induction on l1,then it become

false=true.

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 H1`

which splits the goal into all ways in which H1 could be valid - which are none`congruence`

which is a decision procedure for equalities

Thank you.

`subst l1`

or `rewrite H`

could work as well.

Last updated: Jun 25 2024 at 14:01 UTC