H1: (m::m1::t)<> [] ->
f'(a c (m::m1::t))=a::a0::t'
Goal statement:
match
f'(a c (m::m1::t))
with
| [] => false
|h::t=> .....
Which command i should apply to avoid empty list case?
Did you try rewrite H1
?
It works.Thank you.
Last updated: Oct 13 2024 at 01:02 UTC