induction gives me
Warning: Cannot remove foo. [cannot-remove-as-expected,tactics] but the proof goes through anyway, do I need to worry about e.g. unsoundness?
No, you never have to worry about unsoundness introduced by a tactic. The proof term the tactic generates is a correct proof term as indicated by the working
Qed, meaning the kernel checked your proof term successfully. Can you give some context where the error occurs? In particular, are you doing induction on
foo or does any of your intro patterns use the name
I'm not sure why, but removing
From Equations Require Import Equations gets rid of the warning. Regardless, I'm glad to hear it's not the end of the world!
This might be related to the Keep Proof Equalities flag.
This warning typically applies when induction tries to apply a non-dependent induction principle because the inductive type lives in Prop.
but Keep Proof Equalities only impacts injection users, not induction?
Last updated: Sep 23 2023 at 14:01 UTC