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 04 2023 at 19:01 UTC