What is the difference between the tactic noconf H et depelim H ?
noconf H
depelim H
noconf will work on an equality while depelim on anything of inductive type?
noconf
depelim
Essentially, yes
Last updated: Oct 13 2024 at 01:02 UTC