What do you mean? You can write theorems that show plus is associative and commutative for example but that doesn't make the example I gave "equal" in Coq in th

What do you mean? You can write theorems that show plus is associative and commutative for example but that doesn't make the example I gave "equal" in Coq in the sense you normally mean. As I said, it's not intuitive as we're usually very loose in what we mean by "equal".