Stream: Coq users

Topic: false statement

view this post on Zulip pianke (Mar 03 2023 at 16:58):

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?

view this post on Zulip Laurent Théry (Mar 03 2023 at 18:27):

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

Last updated: Oct 13 2024 at 01:02 UTC