H: f2 a b c (a'::t)=true Goal: f2 a b c []= true

While f2 a b c [] =>false by definition. Is this contra statement?

so the tactic simpl simplifies f2 a b c [] into false but what simpl in H does?

simpl

f2 a b c []

false

simpl in H

Last updated: Oct 04 2023 at 22:01 UTC